# HG changeset patch # User nipkow # Date 864285628 -7200 # Node ID c31e6239d4c93938c12810529f1c14fce82d0b83 # Parent d4ddd43f418a1bbcd12040d2d8ce7435f262d958 Added exhaustion thm and exhaust_tac for each datatype. diff -r d4ddd43f418a -r c31e6239d4c9 src/HOL/NatDef.ML --- a/src/HOL/NatDef.ML Wed May 21 17:31:12 1997 +0200 +++ b/src/HOL/NatDef.ML Thu May 22 09:20:28 1997 +0200 @@ -46,13 +46,6 @@ COND (Datatype.occs_in_prems a (i+1)) all_tac (rename_last_tac a [""] (i+1))]; -(*Install 'automatic' induction tactic, pretending nat is a datatype *) -(*except for induct_tac, everything is dummy*) -datatypes := [("nat",{case_const = Bound 0, case_rewrites = [], - constructors = [], induct_tac = nat_ind_tac, - nchotomy = flexpair_def, case_cong = flexpair_def})]; - - (*A special form of induction for reasoning about m res_inst_tac [("n",v)] natE, + nchotomy = flexpair_def, case_cong = flexpair_def})]; + + (*** Isomorphisms: Abs_Nat and Rep_Nat ***) (*We can't take these properties as axioms, or take Abs_Nat==Inv(Rep_Nat), diff -r d4ddd43f418a -r c31e6239d4c9 src/HOL/datatype.ML --- a/src/HOL/datatype.ML Wed May 21 17:31:12 1997 +0200 +++ b/src/HOL/datatype.ML Thu May 22 09:20:28 1997 +0200 @@ -798,6 +798,21 @@ end handle _ => raise DTYPE_ERR {func="prove_nchotomy", mesg="failed"}; +(*--------------------------------------------------------------------------- + * Turn nchotomy into exhaustion: + * [| !!y1..yi. v = C1 y1..yi ==> P; ...; !!y1..yj. v = Cn y1..yj ==> P |] + * ==> P + *---------------------------------------------------------------------------*) +fun mk_exhaust nchotomy = + let val tac = rtac impI 1 THEN + REPEAT(SOMEGOAL(eresolve_tac [disjE,exE])) + in standard(rule_by_tactic tac (nchotomy RS spec RS rev_mp)) end; + +(* find name of v in exhaustion: *) +fun exhaust_var thm = + let val _ $ ( _ $ Var((x,_),_) $ _ ) = + hd(Logic.strip_assums_hyp(hd(prems_of thm))) + in x end; (*--------------------------------------------------------------------------- * Brings the preceeding functions together. @@ -841,6 +856,9 @@ fun const s = Const(s, the(Sign.const_type sign s)) val case_rewrites = map (fn c => get_fact thy (ty^"_case_"^c)) cl val {nchotomy,case_cong} = case_thms sign case_rewrites itac + val exhaustion = mk_exhaust nchotomy + val exh_var = exhaust_var exhaustion; + fun exhaust_tac a = res_inst_tac [(exh_var,a)] exhaustion; fun induct_tac a i = STATE(fn st => (if Datatype.occs_in_prems a i st @@ -853,6 +871,8 @@ case_rewrites = map mk_rw case_rewrites, induct_tac = induct_tac, nchotomy = nchotomy, + exhaustion = exhaustion, + exhaust_tac = exhaust_tac, case_cong = case_cong}) end end; diff -r d4ddd43f418a -r c31e6239d4c9 src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Wed May 21 17:31:12 1997 +0200 +++ b/src/HOL/simpdata.ML Thu May 22 09:20:28 1997 +0200 @@ -351,7 +351,9 @@ case_rewrites:thm list, constructors:term list, induct_tac: string -> int -> tactic, - nchotomy:thm, + nchotomy: thm, + exhaustion: thm, + exhaust_tac: string -> int -> tactic, case_cong:thm}; exception DT_DATA of (string * dtype_info) list; diff -r d4ddd43f418a -r c31e6239d4c9 src/HOL/thy_data.ML --- a/src/HOL/thy_data.ML Wed May 21 17:31:12 1997 +0200 +++ b/src/HOL/thy_data.ML Thu May 22 09:20:28 1997 +0200 @@ -49,27 +49,48 @@ in (map #case_cong info, flat (map #case_rewrites info)) end; in {case_congs = congs, case_rewrites = rewrites} end; +local + +fun find_tname var Bi = + let val frees = map dest_Free (term_frees Bi) + val params = Logic.strip_params Bi; + in case assoc (frees@params, var) of + None => error("No such variable in subgoal: " ^ quote var) + | Some(Type(tn,_)) => tn + | _ => error("Cannot induct on type of " ^ quote var) + end; + +fun get_dt_info sign tn = + case get_thydata (thyname_of_sign sign) "datatypes" of + None => error ("No such datatype: " ^ quote tn) + | Some (DT_DATA ds) => + case assoc (ds, tn) of + Some info => info + | None => error ("Not a datatype: " ^ quote tn) + +in + (* generic induction tactic for datatypes *) fun induct_tac var i = - let fun find_tname Bi = - let val frees = map dest_Free (term_frees Bi) - val params = Logic.strip_params Bi; - in case assoc (frees@params, var) of - None => error("No such variable in subgoal: " ^ quote var) - | Some(Type(tn,_)) => tn - | _ => error("Cannot induct on type of " ^ quote var) - end; - fun get_ind_tac sign tn = - (case get_thydata (thyname_of_sign sign) "datatypes" of - None => error ("No such datatype: " ^ quote tn) - | Some (DT_DATA ds) => - (case assoc (ds, tn) of - Some {induct_tac, ...} => induct_tac - | None => error ("Not a datatype: " ^ quote tn))); - fun induct state = + let fun induct state = + let val (_, _, Bi, _) = dest_state (state, i) + val sign = #sign(rep_thm state) + val tn = find_tname var Bi + val ind_tac = #induct_tac(get_dt_info sign tn) + in ind_tac var i end + in STATE induct end; + +(* generic exhaustion tactic for datatypes *) +fun exhaust_tac var i = + let fun exhaust state = let val (_, _, Bi, _) = dest_state (state, i) - in get_ind_tac (#sign(rep_thm state)) (find_tname Bi) var i end - in STATE induct end; + val sign = #sign(rep_thm state) + val tn = find_tname var Bi + val exh_tac = #exhaust_tac(get_dt_info sign tn) + in exh_tac var i end + in STATE exhaust end; + +end; (*Must be redefined in order to refer to the new instance of bind_thm created by init_thy_reader.*)