src/HOL/Induct/SList.ML
author paulson
Thu Aug 06 15:48:13 1998 +0200 (1998-08-06)
changeset 5278 a903b66822e2
parent 5223 4cb05273f764
child 5535 678999604ee9
permissions -rw-r--r--
even more tidying of Goal commands
     1 (*  Title:      HOL/ex/SList.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Definition of type 'a list by a least fixed point
     7 *)
     8 
     9 val list_con_defs = [NIL_def, CONS_def];
    10 
    11 Goal "list(A) = {Numb(0)} <+> (A <*> list(A))";
    12 let val rew = rewrite_rule list_con_defs in  
    13 by (fast_tac (claset() addSIs (equalityI :: map rew list.intrs)
    14                       addEs [rew list.elim]) 1)
    15 end;
    16 qed "list_unfold";
    17 
    18 (*This justifies using list in other recursive type definitions*)
    19 Goalw list.defs "A<=B ==> list(A) <= list(B)";
    20 by (rtac lfp_mono 1);
    21 by (REPEAT (ares_tac basic_monos 1));
    22 qed "list_mono";
    23 
    24 (*Type checking -- list creates well-founded sets*)
    25 Goalw (list_con_defs @ list.defs) "list(sexp) <= sexp";
    26 by (rtac lfp_lowerbound 1);
    27 by (fast_tac (claset() addIs sexp.intrs@[sexp_In0I,sexp_In1I]) 1);
    28 qed "list_sexp";
    29 
    30 (* A <= sexp ==> list(A) <= sexp *)
    31 bind_thm ("list_subset_sexp", ([list_mono, list_sexp] MRS subset_trans));
    32 
    33 (*Induction for the type 'a list *)
    34 val prems = goalw SList.thy [Nil_def,Cons_def]
    35     "[| P(Nil);   \
    36 \       !!x xs. P(xs) ==> P(x # xs) |]  ==> P(l)";
    37 by (rtac (Rep_list_inverse RS subst) 1);   (*types force good instantiation*)
    38 by (rtac (Rep_list RS list.induct) 1);
    39 by (REPEAT (ares_tac prems 1
    40      ORELSE eresolve_tac [rangeE, ssubst, Abs_list_inverse RS subst] 1));
    41 qed "list_induct2";
    42 
    43 (*Perform induction on xs. *)
    44 fun list_ind_tac a M = 
    45     EVERY [res_inst_tac [("l",a)] list_induct2 M,
    46            rename_last_tac a ["1"] (M+1)];
    47 
    48 (*** Isomorphisms ***)
    49 
    50 Goal "inj(Rep_list)";
    51 by (rtac inj_inverseI 1);
    52 by (rtac Rep_list_inverse 1);
    53 qed "inj_Rep_list";
    54 
    55 Goal "inj_on Abs_list (list(range Leaf))";
    56 by (rtac inj_on_inverseI 1);
    57 by (etac Abs_list_inverse 1);
    58 qed "inj_on_Abs_list";
    59 
    60 (** Distinctness of constructors **)
    61 
    62 Goalw list_con_defs "CONS M N ~= NIL";
    63 by (rtac In1_not_In0 1);
    64 qed "CONS_not_NIL";
    65 bind_thm ("NIL_not_CONS", (CONS_not_NIL RS not_sym));
    66 
    67 bind_thm ("CONS_neq_NIL", (CONS_not_NIL RS notE));
    68 val NIL_neq_CONS = sym RS CONS_neq_NIL;
    69 
    70 Goalw [Nil_def,Cons_def] "x # xs ~= Nil";
    71 by (rtac (CONS_not_NIL RS (inj_on_Abs_list RS inj_on_contraD)) 1);
    72 by (REPEAT (resolve_tac (list.intrs @ [rangeI, Rep_list]) 1));
    73 qed "Cons_not_Nil";
    74 
    75 bind_thm ("Nil_not_Cons", Cons_not_Nil RS not_sym);
    76 
    77 (** Injectiveness of CONS and Cons **)
    78 
    79 Goalw [CONS_def] "(CONS K M=CONS L N) = (K=L & M=N)";
    80 by (fast_tac (claset() addSEs [Scons_inject, make_elim In1_inject]) 1);
    81 qed "CONS_CONS_eq";
    82 
    83 (*For reasoning about abstract list constructors*)
    84 AddIs ([Rep_list] @ list.intrs);
    85 
    86 AddIffs [CONS_not_NIL, NIL_not_CONS, CONS_CONS_eq];
    87 
    88 AddSDs [inj_on_Abs_list RS inj_onD,
    89         inj_Rep_list RS injD, Leaf_inject];
    90 
    91 Goalw [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)";
    92 by (Fast_tac 1);
    93 qed "Cons_Cons_eq";
    94 bind_thm ("Cons_inject2", (Cons_Cons_eq RS iffD1 RS conjE));
    95 
    96 val [major] = goal SList.thy "CONS M N: list(A) ==> M: A & N: list(A)";
    97 by (rtac (major RS setup_induction) 1);
    98 by (etac list.induct 1);
    99 by (ALLGOALS (Fast_tac));
   100 qed "CONS_D";
   101 
   102 val prems = goalw SList.thy [CONS_def,In1_def]
   103     "CONS M N: sexp ==> M: sexp & N: sexp";
   104 by (cut_facts_tac prems 1);
   105 by (fast_tac (claset() addSDs [Scons_D]) 1);
   106 qed "sexp_CONS_D";
   107 
   108 
   109 (*Reasoning about constructors and their freeness*)
   110 Addsimps list.intrs;
   111 
   112 AddIffs [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq];
   113 
   114 Goal "N: list(A) ==> !M. N ~= CONS M N";
   115 by (etac list.induct 1);
   116 by (ALLGOALS Asm_simp_tac);
   117 qed "not_CONS_self";
   118 
   119 Goal "!x. l ~= x#l";
   120 by (list_ind_tac "l" 1);
   121 by (ALLGOALS Asm_simp_tac);
   122 qed "not_Cons_self2";
   123 
   124 
   125 Goal "(xs ~= []) = (? y ys. xs = y#ys)";
   126 by (list_ind_tac "xs" 1);
   127 by (Simp_tac 1);
   128 by (Asm_simp_tac 1);
   129 by (REPEAT(resolve_tac [exI,refl,conjI] 1));
   130 qed "neq_Nil_conv2";
   131 
   132 (** Conversion rules for List_case: case analysis operator **)
   133 
   134 Goalw [List_case_def,NIL_def] "List_case c h NIL = c";
   135 by (rtac Case_In0 1);
   136 qed "List_case_NIL";
   137 
   138 Goalw [List_case_def,CONS_def]  "List_case c h (CONS M N) = h M N";
   139 by (Simp_tac 1);
   140 qed "List_case_CONS";
   141 
   142 Addsimps [List_case_NIL, List_case_CONS];
   143 
   144 
   145 (*** List_rec -- by wf recursion on pred_sexp ***)
   146 
   147 (* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not
   148    hold if pred_sexp^+ were changed to pred_sexp. *)
   149 
   150 Goal "(%M. List_rec M c d) = wfrec (trancl pred_sexp) \
   151                            \     (%g. List_case c (%x y. d x y (g y)))";
   152 by (simp_tac (HOL_ss addsimps [List_rec_def]) 1);
   153 val List_rec_unfold = standard 
   154   ((wf_pred_sexp RS wf_trancl) RS ((result() RS eq_reflection) RS def_wfrec));
   155 
   156 (*---------------------------------------------------------------------------
   157  * Old:
   158  * val List_rec_unfold = [List_rec_def,wf_pred_sexp RS wf_trancl] MRS def_wfrec
   159  *                     |> standard;
   160  *---------------------------------------------------------------------------*)
   161 
   162 (** pred_sexp lemmas **)
   163 
   164 Goalw [CONS_def,In1_def]
   165     "[| M: sexp;  N: sexp |] ==> (M, CONS M N) : pred_sexp^+";
   166 by (Asm_simp_tac 1);
   167 qed "pred_sexp_CONS_I1";
   168 
   169 Goalw [CONS_def,In1_def]
   170     "[| M: sexp;  N: sexp |] ==> (N, CONS M N) : pred_sexp^+";
   171 by (Asm_simp_tac 1);
   172 qed "pred_sexp_CONS_I2";
   173 
   174 val [prem] = goal SList.thy
   175     "(CONS M1 M2, N) : pred_sexp^+ ==> \
   176 \    (M1,N) : pred_sexp^+ & (M2,N) : pred_sexp^+";
   177 by (rtac (prem RS (pred_sexp_subset_Sigma RS trancl_subset_Sigma RS 
   178                    subsetD RS SigmaE2)) 1);
   179 by (etac (sexp_CONS_D RS conjE) 1);
   180 by (REPEAT (ares_tac [conjI, pred_sexp_CONS_I1, pred_sexp_CONS_I2,
   181                       prem RSN (2, trans_trancl RS transD)] 1));
   182 qed "pred_sexp_CONS_D";
   183 
   184 (** Conversion rules for List_rec **)
   185 
   186 Goal "List_rec NIL c h = c";
   187 by (rtac (List_rec_unfold RS trans) 1);
   188 by (Simp_tac 1);
   189 qed "List_rec_NIL";
   190 
   191 Goal "[| M: sexp;  N: sexp |] ==> \
   192 \    List_rec (CONS M N) c h = h M N (List_rec N c h)";
   193 by (rtac (List_rec_unfold RS trans) 1);
   194 by (asm_simp_tac (simpset() addsimps [pred_sexp_CONS_I2]) 1);
   195 qed "List_rec_CONS";
   196 
   197 Addsimps [List_rec_NIL, List_rec_CONS];
   198 
   199 
   200 (*** list_rec -- by List_rec ***)
   201 
   202 val Rep_list_in_sexp =
   203     [range_Leaf_subset_sexp RS list_subset_sexp, Rep_list] MRS subsetD;
   204 
   205 local
   206   val list_rec_simps = [Abs_list_inverse, Rep_list_inverse,
   207                         Rep_list, rangeI, inj_Leaf, inv_f_f,
   208                         sexp.LeafI, Rep_list_in_sexp]
   209 in
   210   val list_rec_Nil = prove_goalw SList.thy [list_rec_def, Nil_def]
   211       "list_rec Nil c h = c"
   212    (fn _=> [simp_tac (simpset() addsimps list_rec_simps) 1]);
   213 
   214   val list_rec_Cons = prove_goalw SList.thy [list_rec_def, Cons_def]
   215       "list_rec (a#l) c h = h a l (list_rec l c h)"
   216    (fn _=> [simp_tac (simpset() addsimps list_rec_simps) 1]);
   217 end;
   218 
   219 Addsimps [List_rec_NIL, List_rec_CONS, list_rec_Nil, list_rec_Cons];
   220 
   221 
   222 (*Type checking.  Useful?*)
   223 val major::A_subset_sexp::prems = goal SList.thy
   224     "[| M: list(A);     \
   225 \       A<=sexp;        \
   226 \       c: C(NIL);      \
   227 \       !!x y r. [| x: A;  y: list(A);  r: C(y) |] ==> h x y r: C(CONS x y) \
   228 \    |] ==> List_rec M c h : C(M :: 'a item)";
   229 val sexp_ListA_I = A_subset_sexp RS list_subset_sexp RS subsetD;
   230 val sexp_A_I = A_subset_sexp RS subsetD;
   231 by (rtac (major RS list.induct) 1);
   232 by (ALLGOALS(asm_simp_tac (simpset() addsimps ([sexp_A_I,sexp_ListA_I]@prems))));
   233 qed "List_rec_type";
   234 
   235 (** Generalized map functionals **)
   236 
   237 Goalw [Rep_map_def] "Rep_map f Nil = NIL";
   238 by (rtac list_rec_Nil 1);
   239 qed "Rep_map_Nil";
   240 
   241 Goalw [Rep_map_def]
   242     "Rep_map f (x#xs) = CONS (f x) (Rep_map f xs)";
   243 by (rtac list_rec_Cons 1);
   244 qed "Rep_map_Cons";
   245 
   246 val prems = Goalw [Rep_map_def] "(!!x. f(x): A) ==> Rep_map f xs: list(A)";
   247 by (rtac list_induct2 1);
   248 by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
   249 qed "Rep_map_type";
   250 
   251 Goalw [Abs_map_def] "Abs_map g NIL = Nil";
   252 by (rtac List_rec_NIL 1);
   253 qed "Abs_map_NIL";
   254 
   255 val prems = goalw SList.thy [Abs_map_def]
   256     "[| M: sexp;  N: sexp |] ==> \
   257 \    Abs_map g (CONS M N) = g(M) # Abs_map g N";
   258 by (REPEAT (resolve_tac (List_rec_CONS::prems) 1));
   259 qed "Abs_map_CONS";
   260 
   261 (*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
   262 val [rew] = goal SList.thy
   263     "[| !!xs. f(xs) == list_rec xs c h |] ==> f([]) = c";
   264 by (rewtac rew);
   265 by (rtac list_rec_Nil 1);
   266 qed "def_list_rec_Nil";
   267 
   268 val [rew] = goal SList.thy
   269     "[| !!xs. f(xs) == list_rec xs c h |] ==> f(x#xs) = h x xs (f xs)";
   270 by (rewtac rew);
   271 by (rtac list_rec_Cons 1);
   272 qed "def_list_rec_Cons";
   273 
   274 fun list_recs def =
   275       [standard (def RS def_list_rec_Nil),
   276        standard (def RS def_list_rec_Cons)];
   277 
   278 (*** Unfolding the basic combinators ***)
   279 
   280 val [null_Nil, null_Cons]               = list_recs null_def;
   281 val [_, hd_Cons]                        = list_recs hd_def;
   282 val [_, tl_Cons]                        = list_recs tl_def;
   283 val [ttl_Nil, ttl_Cons]                 = list_recs ttl_def;
   284 val [append_Nil3, append_Cons]          = list_recs append_def;
   285 val [mem_Nil, mem_Cons]                 = list_recs mem_def;
   286 val [set_Nil, set_Cons]                 = list_recs set_def;
   287 val [map_Nil, map_Cons]                 = list_recs map_def;
   288 val [list_case_Nil, list_case_Cons]     = list_recs list_case_def;
   289 val [filter_Nil, filter_Cons]           = list_recs filter_def;
   290 
   291 Addsimps
   292   [null_Nil, ttl_Nil,
   293    mem_Nil, mem_Cons,
   294    list_case_Nil, list_case_Cons,
   295    append_Nil3, append_Cons,
   296    set_Nil, set_Cons, 
   297    map_Nil, map_Cons,
   298    filter_Nil, filter_Cons];
   299 
   300 
   301 (** @ - append **)
   302 
   303 Goal "(xs@ys)@zs = xs@(ys@zs)";
   304 by (list_ind_tac "xs" 1);
   305 by (ALLGOALS Asm_simp_tac);
   306 qed "append_assoc2";
   307 
   308 Goal "xs @ [] = xs";
   309 by (list_ind_tac "xs" 1);
   310 by (ALLGOALS Asm_simp_tac);
   311 qed "append_Nil4";
   312 
   313 (** mem **)
   314 
   315 Goal "x mem (xs@ys) = (x mem xs | x mem ys)";
   316 by (list_ind_tac "xs" 1);
   317 by (ALLGOALS Asm_simp_tac);
   318 qed "mem_append2";
   319 
   320 Goal "x mem [x:xs. P(x)] = (x mem xs & P(x))";
   321 by (list_ind_tac "xs" 1);
   322 by (ALLGOALS Asm_simp_tac);
   323 qed "mem_filter2";
   324 
   325 
   326 (** The functional "map" **)
   327 
   328 Addsimps [Rep_map_Nil, Rep_map_Cons, Abs_map_NIL, Abs_map_CONS];
   329 
   330 val [major,A_subset_sexp,minor] = goal SList.thy 
   331     "[| M: list(A);  A<=sexp;  !!z. z: A ==> f(g(z)) = z |] \
   332 \    ==> Rep_map f (Abs_map g M) = M";
   333 by (rtac (major RS list.induct) 1);
   334 by (ALLGOALS (asm_simp_tac (simpset() addsimps [sexp_A_I,sexp_ListA_I,minor])));
   335 qed "Abs_map_inverse";
   336 
   337 (*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*)
   338 
   339 (** list_case **)
   340 
   341 Goal "P(list_case a f xs) = ((xs=[] --> P(a)) & \
   342 \                        (!y ys. xs=y#ys --> P(f y ys)))";
   343 by (list_ind_tac "xs" 1);
   344 by (ALLGOALS Asm_simp_tac);
   345 qed "split_list_case2";
   346 
   347 
   348 (** Additional mapping lemmas **)
   349 
   350 Goal "map (%x. x) xs = xs";
   351 by (list_ind_tac "xs" 1);
   352 by (ALLGOALS Asm_simp_tac);
   353 qed "map_ident2";
   354 
   355 Goal "map f (xs@ys) = map f xs @ map f ys";
   356 by (list_ind_tac "xs" 1);
   357 by (ALLGOALS Asm_simp_tac);
   358 qed "map_append2";
   359 
   360 Goalw [o_def] "map (f o g) xs = map f (map g xs)";
   361 by (list_ind_tac "xs" 1);
   362 by (ALLGOALS Asm_simp_tac);
   363 qed "map_compose2";
   364 
   365 val prems = 
   366 Goal "(!!x. f(x): sexp) ==> \
   367 \       Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs";
   368 by (list_ind_tac "xs" 1);
   369 by (ALLGOALS (asm_simp_tac(simpset() addsimps
   370 			   (prems@[Rep_map_type, list_sexp RS subsetD]))));
   371 qed "Abs_Rep_map";
   372 
   373 Addsimps [append_Nil4, map_ident2];