# HG changeset patch
# User nipkow
# Date 760265747 -3600
# Node ID ac7b7003f17743122f8f22a13a1e30ceb37d3bc5
# Parent  91614f0eb250dea55fd3ebde03bd0a670664be13
Introduction of various new lemmas and of case_tac.

diff -r 91614f0eb250 -r ac7b7003f177 Arith.ML
--- a/Arith.ML	Thu Jan 27 17:01:10 1994 +0100
+++ b/Arith.ML	Thu Feb 03 09:55:47 1994 +0100
@@ -228,3 +228,9 @@
 
 val less_add_Suc1 = standard (lessI RS (le_add1 RS le_less_trans));
 val less_add_Suc2 = standard (lessI RS (le_add2 RS le_less_trans));
+
+goal Arith.thy "m+k<=n --> m<=n::nat";
+by(nat_ind_tac "k" 1);
+by(ALLGOALS(simp_tac arith_ss));
+by(fast_tac (HOL_cs addDs [Suc_leD]) 1);
+val plus_leD1 = result() RS mp;
diff -r 91614f0eb250 -r ac7b7003f177 HOL.ML
--- a/HOL.ML	Thu Jan 27 17:01:10 1994 +0100
+++ b/HOL.ML	Thu Feb 03 09:55:47 1994 +0100
@@ -17,6 +17,7 @@
   val arg_cong: thm
   val fun_cong: thm
   val box_equals: thm
+  val case_tac: string -> int -> tactic
   val ccontr: thm
   val classical: thm
   val cong: thm
@@ -322,6 +323,14 @@
  (fn major::prems=>
   [ rtac ccontr 1, rtac (major RS notE) 1, REPEAT (ares_tac prems 1)]);
 
+(* case distinction *)
+
+val case_split_thm = prove_goal HOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q"
+  (fn [p1,p2] => [cut_facts_tac [excluded_middle] 1, etac disjE 1,
+                  etac p2 1, etac p1 1]);
+
+fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
+
 (** Standard abbreviations **)
 
 fun stac th = rtac(th RS ssubst);
@@ -331,4 +340,3 @@
 end;
 
 open HOL_Lemmas;
-
diff -r 91614f0eb250 -r ac7b7003f177 List.ML
--- a/List.ML	Thu Jan 27 17:01:10 1994 +0100
+++ b/List.ML	Thu Feb 03 09:55:47 1994 +0100
@@ -163,6 +163,13 @@
 val not_Cons_self = result();
 
 
+goal List.thy "(xs ~= []) = (? y ys. xs = Cons(y,ys))";
+by(list_ind_tac "xs" 1);
+by(simp_tac list_free_ss 1);
+by(asm_simp_tac list_free_ss 1);
+by(REPEAT(resolve_tac [exI,refl,conjI] 1));
+val neq_Nil_conv = result();
+
 (** Conversion rules for List_case: case analysis operator **)
 
 goalw List.thy [List_case_def,NIL_def] "List_case(NIL,c,h) = c";
@@ -303,6 +310,7 @@
 val [null_Nil,null_Cons] = list_recs null_def;
 val [_,hd_Cons] = list_recs hd_def;
 val [_,tl_Cons] = list_recs tl_def;
+val [ttl_Nil,ttl_Cons] = list_recs ttl_def;
 val [append_Nil,append_Cons] = list_recs append_def;
 val [mem_Nil, mem_Cons] = list_recs mem_def;
 val [map_Nil,map_Cons] = list_recs map_def;
@@ -313,7 +321,7 @@
 val list_ss = arith_ss addsimps
   [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq,
    list_rec_Nil, list_rec_Cons,
-   null_Nil, null_Cons, hd_Cons, tl_Cons,
+   null_Nil, null_Cons, hd_Cons, tl_Cons, ttl_Nil, ttl_Cons,
    mem_Nil, mem_Cons,
    list_case_Nil, list_case_Cons,
    append_Nil, append_Cons,
@@ -329,6 +337,11 @@
 by(ALLGOALS(asm_simp_tac list_ss));
 val append_assoc = result();
 
+goal List.thy "xs @ [] = xs";
+by(list_ind_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac list_ss));
+val append_Nil2 = result();
+
 (** mem **)
 
 goal List.thy "x mem (xs@ys) = (x mem xs | x mem ys)";
@@ -376,6 +389,16 @@
 
 (*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*)
 
+(** list_case **)
+
+goal List.thy
+ "P(list_case(xs,a,f)) = ((xs=[] --> P(a)) & \
+\                         (!y ys. xs=Cons(y,ys) --> P(f(y,ys))))";
+by(list_ind_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac (list_ss addsimps [list_case_Nil,list_case_Cons])));
+by(fast_tac HOL_cs 1);
+val expand_list_case = result();
+
 
 (** Additional mapping lemmas **)
 
@@ -392,5 +415,6 @@
 val Abs_Rep_map = result();
 
 val list_ss = list_ss addsimps
-  [mem_append, mem_filter, append_assoc, map_ident,
+  [mem_append, mem_filter, append_assoc, append_Nil2, map_ident,
    list_all_True, list_all_conj];
+
diff -r 91614f0eb250 -r ac7b7003f177 List.thy
--- a/List.thy	Thu Jan 27 17:01:10 1994 +0100
+++ b/List.thy	Thu Feb 03 09:55:47 1994 +0100
@@ -36,7 +36,7 @@
   Abs_map       :: "('a node set => 'b) => 'a node set => 'b list"
   null          :: "'a list => bool"
   hd            :: "'a list => 'a"
-  tl            :: "'a list => 'a list"
+  tl,ttl        :: "'a list => 'a list"
   mem		:: "['a, 'a list] => bool"			(infixl 55)
   list_all      :: "('a => bool) => ('a list => bool)"
   map           :: "('a=>'b) => ('a list => 'b list)"
@@ -104,6 +104,8 @@
   null_def      "null(xs)            == list_rec(xs, True, %x xs r.False)"
   hd_def        "hd(xs)              == list_rec(xs, @x.True, %x xs r.x)"
   tl_def        "tl(xs)              == list_rec(xs, @xs.True, %x xs r.xs)"
+  (* a total version of tl: *)
+  ttl_def	"ttl(xs)             == list_rec(xs, [], %x xs r.xs)"
   mem_def	"x mem xs            == \
 \		   list_rec(xs, False, %y ys r. if(y=x, True, r))"
   list_all_def  "list_all(P, xs)     == list_rec(xs, True, %x l r. P(x) & r)"
diff -r 91614f0eb250 -r ac7b7003f177 Nat.ML
--- a/Nat.ML	Thu Jan 27 17:01:10 1994 +0100
+++ b/Nat.ML	Thu Feb 03 09:55:47 1994 +0100
@@ -379,6 +379,11 @@
 by (fast_tac (HOL_cs addEs [less_anti_refl,less_anti_sym]) 1);
 val lessD = result();
 
+goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
+by(asm_full_simp_tac (HOL_ss addsimps [less_Suc_eq]) 1);
+by(fast_tac HOL_cs 1);
+val Suc_leD = result();
+
 goalw Nat.thy [le_def] "!!m. m < n ==> m <= n::nat";
 by (fast_tac (HOL_cs addEs [less_anti_sym]) 1);
 val less_imp_le = result();
diff -r 91614f0eb250 -r ac7b7003f177 arith.ML
--- a/arith.ML	Thu Jan 27 17:01:10 1994 +0100
+++ b/arith.ML	Thu Feb 03 09:55:47 1994 +0100
@@ -228,3 +228,9 @@
 
 val less_add_Suc1 = standard (lessI RS (le_add1 RS le_less_trans));
 val less_add_Suc2 = standard (lessI RS (le_add2 RS le_less_trans));
+
+goal Arith.thy "m+k<=n --> m<=n::nat";
+by(nat_ind_tac "k" 1);
+by(ALLGOALS(simp_tac arith_ss));
+by(fast_tac (HOL_cs addDs [Suc_leD]) 1);
+val plus_leD1 = result() RS mp;
diff -r 91614f0eb250 -r ac7b7003f177 hol.ML
--- a/hol.ML	Thu Jan 27 17:01:10 1994 +0100
+++ b/hol.ML	Thu Feb 03 09:55:47 1994 +0100
@@ -17,6 +17,7 @@
   val arg_cong: thm
   val fun_cong: thm
   val box_equals: thm
+  val case_tac: string -> int -> tactic
   val ccontr: thm
   val classical: thm
   val cong: thm
@@ -322,6 +323,14 @@
  (fn major::prems=>
   [ rtac ccontr 1, rtac (major RS notE) 1, REPEAT (ares_tac prems 1)]);
 
+(* case distinction *)
+
+val case_split_thm = prove_goal HOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q"
+  (fn [p1,p2] => [cut_facts_tac [excluded_middle] 1, etac disjE 1,
+                  etac p2 1, etac p1 1]);
+
+fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
+
 (** Standard abbreviations **)
 
 fun stac th = rtac(th RS ssubst);
@@ -331,4 +340,3 @@
 end;
 
 open HOL_Lemmas;
-
diff -r 91614f0eb250 -r ac7b7003f177 nat.ML
--- a/nat.ML	Thu Jan 27 17:01:10 1994 +0100
+++ b/nat.ML	Thu Feb 03 09:55:47 1994 +0100
@@ -379,6 +379,11 @@
 by (fast_tac (HOL_cs addEs [less_anti_refl,less_anti_sym]) 1);
 val lessD = result();
 
+goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
+by(asm_full_simp_tac (HOL_ss addsimps [less_Suc_eq]) 1);
+by(fast_tac HOL_cs 1);
+val Suc_leD = result();
+
 goalw Nat.thy [le_def] "!!m. m < n ==> m <= n::nat";
 by (fast_tac (HOL_cs addEs [less_anti_sym]) 1);
 val less_imp_le = result();
diff -r 91614f0eb250 -r ac7b7003f177 simpdata.ML
--- a/simpdata.ML	Thu Jan 27 17:01:10 1994 +0100
+++ b/simpdata.ML	Thu Feb 03 09:55:47 1994 +0100
@@ -52,6 +52,7 @@
 val simp_thms = map prover
  [ "(x=x) = True",
    "(~True) = False", "(~False) = True", "(~ ~ P) = P",
+   "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
    "(True=P) = P", "(P=True) = P",
    "(True --> P) = P", "(False --> P) = True", 
    "(P --> True) = True", "(P --> P) = True",
@@ -101,6 +102,17 @@
 fun split_tac splits =
   mk_case_split_tac (meta_obj_reflection RS iffD2) (map mk_eq splits);
 
+(* eliminiation of existential quantifiers in assumptions *)
+
+val ex_all_equiv =
+  let val lemma1 = prove_goal HOL.thy
+        "(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)"
+        (fn prems => [resolve_tac prems 1, etac exI 1]);
+      val lemma2 = prove_goalw HOL.thy [Ex_def RS eq_reflection]
+        "(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)"
+        (fn prems => [REPEAT(resolve_tac prems 1)])
+  in equal_intr lemma1 lemma2 end;
+
 (** '&' congruence rule: not included by default! *)
 
 val conj_cong = impI RSN