# HG changeset patch # User paulson # Date 915625473 -3600 # Node ID 3b4a29166f26807136db8a1f6e6ea9644978e302 # Parent 0786b5afd8eebd8490435723b121c69c85a7e995 induct_tac and exhaust_tac diff -r 0786b5afd8ee -r 3b4a29166f26 src/ZF/Integ/Bin.ML --- a/src/ZF/Integ/Bin.ML Wed Jan 06 13:23:41 1999 +0100 +++ b/src/ZF/Integ/Bin.ML Wed Jan 06 13:24:33 1999 +0100 @@ -10,13 +10,6 @@ Addsimps bin.intrs; Addsimps int_typechecks; -(*Perform induction on l, then prove the major premise using prems. *) -fun bin_ind_tac a prems i = - EVERY [res_inst_tac [("x",a)] bin.induct i, - rename_last_tac a ["1"] (i+3), - ares_tac prems i]; - - Goal "NCons(Pls,0) = Pls"; by (Asm_simp_tac 1); qed "NCons_Pls_0"; @@ -48,46 +41,47 @@ Addsimps [bool_into_nat]; Goal "w: bin ==> integ_of(w) : int"; -by (bin_ind_tac "w" [] 1); +by (induct_tac "w" 1); by (ALLGOALS (Asm_simp_tac)); qed "integ_of_type"; Addsimps [integ_of_type]; Goal "[| w: bin; b: bool |] ==> NCons(w,b) : bin"; -by (bin_ind_tac "w" [] 1); +by (induct_tac "w" 1); by Auto_tac; qed "NCons_type"; Addsimps [NCons_type]; Goal "w: bin ==> bin_succ(w) : bin"; -by (bin_ind_tac "w" [] 1); +by (induct_tac "w" 1); by Auto_tac; qed "bin_succ_type"; Addsimps [bin_succ_type]; Goal "w: bin ==> bin_pred(w) : bin"; -by (bin_ind_tac "w" [] 1); +by (induct_tac "w" 1); by Auto_tac; qed "bin_pred_type"; Addsimps [bin_pred_type]; Goal "w: bin ==> bin_minus(w) : bin"; -by (bin_ind_tac "w" [] 1); +by (induct_tac "w" 1); by Auto_tac; qed "bin_minus_type"; Addsimps [bin_minus_type]; (*This proof is complicated by the mutual recursion*) Goal "v: bin ==> ALL w: bin. bin_add(v,w) : bin"; -by (bin_ind_tac "v" [] 1); +by (induct_tac "v" 1); by (rtac ballI 3); -by (bin_ind_tac "w" [] 3); +by (rename_tac "w'" 3); +by (induct_tac "w'" 3); by Auto_tac; bind_thm ("bin_add_type", result() RS bspec); Addsimps [bin_add_type]; Goal "[| v: bin; w: bin |] ==> bin_mult(v,w) : bin"; -by (bin_ind_tac "v" [] 1); +by (induct_tac "v" 1); by Auto_tac; qed "bin_mult_type"; Addsimps [bin_mult_type]; @@ -173,7 +167,7 @@ by (Simp_tac 1); by (Simp_tac 1); by (rtac ballI 1); -by (bin_ind_tac "wa" [] 1); +by (induct_tac "wa" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac setloop (etac boolE)))); bind_thm("integ_of_add", result() RS bspec); @@ -184,13 +178,12 @@ Goal "[| v: bin; w: bin |] \ \ ==> integ_of(bin_mult(v,w)) = integ_of(v) $* integ_of(w)"; -by (bin_ind_tac "v" [major] 1); +by (induct_tac "v" 1); by (Asm_simp_tac 1); by (Asm_simp_tac 1); by (etac boolE 1); by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 2); -by (asm_simp_tac - (simpset() addsimps [zadd_zmult_distrib] @ zadd_ac) 1); +by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib] @ zadd_ac) 1); qed "integ_of_mult"; (**** Computations ****) diff -r 0786b5afd8ee -r 3b4a29166f26 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Wed Jan 06 13:23:41 1999 +0100 +++ b/src/ZF/IsaMakefile Wed Jan 06 13:24:33 1999 +0100 @@ -43,7 +43,7 @@ ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML subset.ML \ subset.thy thy_syntax.ML upair.ML upair.thy \ Tools/cartprod.ML Tools/datatype_package.ML Tools/inductive_package.ML \ - Tools/primrec_package.ML Tools/typechk.ML \ + Tools/primrec_package.ML Tools/induct_tacs.ML Tools/typechk.ML \ Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy \ Integ/twos_compl.ML Integ/Bin.ML Integ/Bin.thy @$(ISATOOL) usedir -b $(OUT)/FOL ZF diff -r 0786b5afd8ee -r 3b4a29166f26 src/ZF/List.ML --- a/src/ZF/List.ML Wed Jan 06 13:23:41 1999 +0100 +++ b/src/ZF/List.ML Wed Jan 06 13:24:33 1999 +0100 @@ -15,12 +15,6 @@ val Cons_iff = list.mk_free "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'"; val Nil_Cons_iff = list.mk_free "~ Nil=Cons(a,l)"; -(*Perform induction on l, then prove the major premise using prems. *) -fun list_ind_tac a prems i = - EVERY [res_inst_tac [("x",a)] list.induct i, - rename_last_tac a ["1"] (i+2), - ares_tac prems i]; - Goal "list(A) = {0} + (A * list(A))"; let open list; val rew = rewrite_rule con_defs in by (blast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1) @@ -63,7 +57,7 @@ (*** List functions ***) Goal "l: list(A) ==> tl(l) : list(A)"; -by (etac list.elim 1); +by (exhaust_tac "l" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps list.intrs))); qed "tl_type"; @@ -102,7 +96,8 @@ \ c: C(Nil); \ \ !!x y r. [| x:A; y: list(A); r: C(y) |] ==> h(x,y,r): C(Cons(x,y)) \ \ |] ==> list_rec(c,h,l) : C(l)"; -by (list_ind_tac "l" prems 1); +by (cut_facts_tac prems 1); +by (induct_tac "l" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); qed "list_rec_type"; @@ -183,29 +178,29 @@ (*** theorems about map ***) Goal "l: list(A) ==> map(%u. u, l) = l"; -by (list_ind_tac "l" [] 1); +by (induct_tac "l" 1); by (ALLGOALS Asm_simp_tac); qed "map_ident"; Goal "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)"; -by (list_ind_tac "l" [] 1); +by (induct_tac "l" 1); by (ALLGOALS Asm_simp_tac); qed "map_compose"; Goal "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)"; -by (list_ind_tac "xs" [] 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed "map_app_distrib"; Goal "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))"; -by (list_ind_tac "ls" [] 1); +by (induct_tac "ls" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib]))); qed "map_flat"; Goal "l: list(A) ==> \ \ list_rec(c, d, map(h,l)) = \ \ list_rec(c, %x xs r. d(h(x), map(h,xs), r), l)"; -by (list_ind_tac "l" [] 1); +by (induct_tac "l" 1); by (ALLGOALS Asm_simp_tac); qed "list_rec_map"; @@ -215,19 +210,19 @@ bind_thm ("list_CollectD", (Collect_subset RS list_mono RS subsetD)); Goal "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)"; -by (list_ind_tac "l" [] 1); +by (induct_tac "l" 1); by (ALLGOALS Asm_simp_tac); qed "map_list_Collect"; (*** theorems about length ***) Goal "xs: list(A) ==> length(map(h,xs)) = length(xs)"; -by (list_ind_tac "xs" [] 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed "length_map"; Goal "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)"; -by (list_ind_tac "xs" [] 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed "length_app"; @@ -236,12 +231,12 @@ val add_commute_succ = nat_succI RSN (2,add_commute); Goal "xs: list(A) ==> length(rev(xs)) = length(xs)"; -by (list_ind_tac "xs" [] 1); +by (induct_tac "xs" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app, add_commute_succ]))); qed "length_rev"; Goal "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))"; -by (list_ind_tac "ls" [] 1); +by (induct_tac "ls" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app]))); qed "length_flat"; @@ -279,19 +274,19 @@ qed "app_right_Nil"; Goal "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)"; -by (list_ind_tac "xs" [] 1); +by (induct_tac "xs" 1); by (ALLGOALS Asm_simp_tac); qed "app_assoc"; Goal "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)"; -by (list_ind_tac "ls" [] 1); +by (induct_tac "ls" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_assoc]))); qed "flat_app_distrib"; (*** theorems about rev ***) Goal "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))"; -by (list_ind_tac "l" [] 1); +by (induct_tac "l" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib]))); qed "rev_map_distrib"; @@ -305,12 +300,12 @@ qed "rev_app_distrib"; Goal "l: list(A) ==> rev(rev(l))=l"; -by (list_ind_tac "l" [] 1); +by (induct_tac "l" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [rev_app_distrib]))); qed "rev_rev_ident"; Goal "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))"; -by (list_ind_tac "ls" [] 1); +by (induct_tac "ls" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil]))); qed "rev_flat"; @@ -320,7 +315,7 @@ Goal "[| xs: list(nat); ys: list(nat) |] ==> \ \ list_add(xs@ys) = list_add(ys) #+ list_add(xs)"; -by (list_ind_tac "xs" [] 1); +by (induct_tac "xs" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_0_right, add_assoc RS sym]))); by (rtac (add_commute RS subst_context) 1); @@ -328,13 +323,13 @@ qed "list_add_app"; Goal "l: list(nat) ==> list_add(rev(l)) = list_add(l)"; -by (list_ind_tac "l" [] 1); +by (induct_tac "l" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [list_add_app, add_0_right]))); qed "list_add_rev"; Goal "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))"; -by (list_ind_tac "ls" [] 1); +by (induct_tac "ls" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [list_add_app]))); by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1)); qed "list_add_flat"; diff -r 0786b5afd8ee -r 3b4a29166f26 src/ZF/ROOT.ML --- a/src/ZF/ROOT.ML Wed Jan 06 13:23:41 1999 +0100 +++ b/src/ZF/ROOT.ML Wed Jan 06 13:24:33 1999 +0100 @@ -46,6 +46,7 @@ use "Tools/datatype_package"; use "Tools/primrec_package"; use_thy "Datatype"; +use "Tools/induct_tacs"; use_thy "InfDatatype"; use_thy "List"; diff -r 0786b5afd8ee -r 3b4a29166f26 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Wed Jan 06 13:23:41 1999 +0100 +++ b/src/ZF/Tools/datatype_package.ML Wed Jan 06 13:24:33 1999 +0100 @@ -1,9 +1,9 @@ -(* Title: ZF/datatype_package.ML +(* Title: ZF/Tools/datatype_package.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge -Fixedpoint definition module -- for Inductive/Codatatype Definitions +Datatype/Codatatype Definitions The functor will be instantiated for normal sums/products (datatype defs) and non-standard sums/products (codatatype defs) @@ -243,7 +243,7 @@ | rec_args ((Const("op :",_)$arg$X)::prems) = (case head_of X of Const(a,_) => (*recursive occurrence?*) - if Sign.base_name a mem_string rec_base_names + if a mem_string rec_names then arg :: rec_args prems else rec_args prems | _ => rec_args prems) diff -r 0786b5afd8ee -r 3b4a29166f26 src/ZF/Tools/induct_tacs.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Tools/induct_tacs.ML Wed Jan 06 13:24:33 1999 +0100 @@ -0,0 +1,68 @@ +(* Title: HOL/Tools/induct_tacs.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Induction and exhaustion tactics for Isabelle/ZF +*) + + +signature DATATYPE_TACTICS = +sig + val induct_tac : string -> int -> tactic + val exhaust_tac : string -> int -> tactic +end; + + +structure DatatypeTactics : DATATYPE_TACTICS = +struct + +fun datatype_info_sg sign name = + (case Symtab.lookup (DatatypesData.get_sg sign, name) of + Some info => info + | None => error ("Unknown datatype " ^ quote name)); + + +(*Given a variable, find the inductive set associated it in the assumptions*) +fun find_tname var Bi = + let fun mk_pair (Const("op :",_) $ Free (v,_) $ A) = + (v, #1 (dest_Const (head_of A))) + | mk_pair _ = raise Match + val pairs = mapfilter (try (mk_pair o FOLogic.dest_Trueprop)) + (#2 (strip_context Bi)) + in case assoc (pairs, var) of + None => error ("Cannot determine datatype of " ^ quote var) + | Some t => t + end; + +(** generic exhaustion and induction tactic for datatypes + Differences from HOL: + (1) no checking if the induction var occurs in premises, since it always + appears in one of them, and it's hard to check for other occurrences + (2) exhaustion works for VARIABLES in the premises, not general terms +**) + +fun exhaust_induct_tac exh var i state = + let + val (_, _, Bi, _) = dest_state (state, i) + val {sign, ...} = rep_thm state + val tn = find_tname var Bi + val rule = + if exh then #exhaustion (datatype_info_sg sign tn) + else #induct (datatype_info_sg sign tn) + val (Const("op :",_) $ Var(ixn,_) $ _) = + FOLogic.dest_Trueprop (hd (prems_of rule)) + val ind_vname = Syntax.string_of_vname ixn + val vname' = (*delete leading question mark*) + String.substring (ind_vname, 1, size ind_vname-1) + in + eres_inst_tac [(vname',var)] rule i state + end; + +val exhaust_tac = exhaust_induct_tac true; +val induct_tac = exhaust_induct_tac false; + +end; + + +open DatatypeTactics; diff -r 0786b5afd8ee -r 3b4a29166f26 src/ZF/Tools/primrec_package.ML --- a/src/ZF/Tools/primrec_package.ML Wed Jan 06 13:23:41 1999 +0100 +++ b/src/ZF/Tools/primrec_package.ML Wed Jan 06 13:24:33 1999 +0100 @@ -149,7 +149,10 @@ $ rec_arg) in - writeln ("def = " ^ Sign.string_of_term (sign_of thy) def_tm); + if !Ind_Syntax.trace then + writeln ("primrec def:\n" ^ + Sign.string_of_term (sign_of thy) def_tm) + else(); (Sign.base_name fname ^ "_" ^ Sign.base_name big_rec_name ^ "_def", def_tm) end; @@ -169,14 +172,16 @@ |> Theory.add_defs_i [def] val rewrites = get_axiom thy' (#1 def) :: map mk_meta_eq (#rec_rewrites con_info) - val _ = writeln ("Proving equations for primrec function " ^ fname); val char_thms = - map (fn (_,t) => - prove_goalw_cterm rewrites - (Ind_Syntax.traceIt "next primrec equation = " - (cterm_of (sign_of thy') t)) - (fn _ => [rtac refl 1])) - recursion_eqns; + (if !Ind_Syntax.trace then + writeln ("Proving equations for primrec function " ^ fname) + else (); + map (fn (_,t) => + prove_goalw_cterm rewrites + (Ind_Syntax.traceIt "next primrec equation = " + (cterm_of (sign_of thy') t)) + (fn _ => [rtac refl 1])) + recursion_eqns); val tsimps = Attribute.tthms_of char_thms; val thy'' = thy' |> PureThy.add_tthmss [(("simps", tsimps), [Simplifier.simp_add_global])] diff -r 0786b5afd8ee -r 3b4a29166f26 src/ZF/Zorn.ML --- a/src/ZF/Zorn.ML Wed Jan 06 13:23:41 1999 +0100 +++ b/src/ZF/Zorn.ML Wed Jan 06 13:24:33 1999 +0100 @@ -49,12 +49,6 @@ by (ALLGOALS (fast_tac (claset() addIs prems))); qed "TFin_induct"; -(*Perform induction on n, then prove the major premise using prems. *) -fun TFin_ind_tac a prems i = - EVERY [res_inst_tac [("n",a)] TFin_induct i, - rename_last_tac a ["1"] (i+1), - rename_last_tac a ["2"] (i+2), - ares_tac prems i]; (*** Section 3. Some Properties of the Transfinite Construction ***) diff -r 0786b5afd8ee -r 3b4a29166f26 src/ZF/ex/BT.ML --- a/src/ZF/ex/BT.ML Wed Jan 06 13:23:41 1999 +0100 +++ b/src/ZF/ex/BT.ML Wed Jan 06 13:24:33 1999 +0100 @@ -6,13 +6,6 @@ Datatype definition of binary trees *) -(*Perform induction on l, then prove the major premise using prems. *) -fun bt_ind_tac a prems i = - EVERY [res_inst_tac [("x",a)] bt.induct i, - rename_last_tac a ["1","2"] (i+2), - ares_tac prems i]; - - Addsimps bt.intrs; (** Lemmas to justify using "bt" in other recursive type definitions **) @@ -34,20 +27,21 @@ (*Type checking -- proved by induction, as usual*) -val prems = goal BT.thy +val major::prems = goal BT.thy "[| t: bt(A); \ \ c: C(Lf); \ \ !!x y z r s. [| x:A; y:bt(A); z:bt(A); r:C(y); s:C(z) |] ==> \ \ h(x,y,z,r,s): C(Br(x,y,z)) \ \ |] ==> bt_rec(c,h,t) : C(t)"; -by (bt_ind_tac "t" prems 1); + (*instead of induct_tac "t", since t: bt(A) isn't an assumption*) +by (rtac (major RS bt.induct) 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); qed "bt_rec_type"; (** n_nodes **) Goal "t: bt(A) ==> n_nodes(t) : nat"; -by (bt_ind_tac "t" [] 1); +by (induct_tac "t" 1); by Auto_tac; qed "n_nodes_type"; @@ -55,14 +49,14 @@ (** n_leaves **) Goal "t: bt(A) ==> n_leaves(t) : nat"; -by (bt_ind_tac "t" [] 1); +by (induct_tac "t" 1); by Auto_tac; qed "n_leaves_type"; (** bt_reflect **) Goal "t: bt(A) ==> bt_reflect(t) : bt(A)"; -by (bt_ind_tac "t" [] 1); +by (induct_tac "t" 1); by Auto_tac; by (REPEAT (ares_tac (bt.intrs @ [bt_rec_type]) 1)); qed "bt_reflect_type"; @@ -76,23 +70,20 @@ (*** theorems about n_leaves ***) -val prems = goal BT.thy - "t: bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)"; -by (bt_ind_tac "t" prems 1); +Goal "t: bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)"; +by (induct_tac "t" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_commute, n_leaves_type]))); qed "n_leaves_reflect"; -val prems = goal BT.thy - "t: bt(A) ==> n_leaves(t) = succ(n_nodes(t))"; -by (bt_ind_tac "t" prems 1); +Goal "t: bt(A) ==> n_leaves(t) = succ(n_nodes(t))"; +by (induct_tac "t" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_succ_right]))); qed "n_leaves_nodes"; (*** theorems about bt_reflect ***) -val prems = goal BT.thy - "t: bt(A) ==> bt_reflect(bt_reflect(t))=t"; -by (bt_ind_tac "t" prems 1); +Goal "t: bt(A) ==> bt_reflect(bt_reflect(t))=t"; +by (induct_tac "t" 1); by (ALLGOALS Asm_simp_tac); qed "bt_reflect_bt_reflect_ident"; diff -r 0786b5afd8ee -r 3b4a29166f26 src/ZF/ex/Primrec.ML --- a/src/ZF/ex/Primrec.ML Wed Jan 06 13:23:41 1999 +0100 +++ b/src/ZF/ex/Primrec.ML Wed Jan 06 13:24:33 1999 +0100 @@ -175,9 +175,8 @@ Addsimps [list_add_type, nat_into_Ord]; -Goalw [SC_def] - "l: list(nat) ==> SC ` l < ack(1, list_add(l))"; -by (etac list.elim 1); +Goalw [SC_def] "l: list(nat) ==> SC ` l < ack(1, list_add(l))"; +by (exhaust_tac "l" 1); by (asm_simp_tac (simpset() addsimps [succ_iff]) 1); by (asm_simp_tac (simpset() addsimps [ack_1, add_le_self]) 1); qed "SC_case"; @@ -258,7 +257,7 @@ \ g: prim_rec; kg: nat; \ \ l: list(nat) \ \ |] ==> PREC(f,g)`l #+ list_add(l) < ack(succ(kf#+kg), list_add(l))"; -by (etac list.elim 1); +by (exhaust_tac "l" 1); by (asm_simp_tac (simpset() addsimps [[nat_le_refl, lt_ack2] MRS lt_trans]) 1); by (Asm_simp_tac 1); by (etac ssubst 1); (*get rid of the needless assumption*)