# HG changeset patch # User wenzelm # Date 951252504 -3600 # Node ID 5928c72b70571b750f166a8047416f61268accb5 # Parent 493707fcd8a6859fff7f2be9b2b7fb3de7fbe17e induct: tuned syntax; added cases method; diff -r 493707fcd8a6 -r 5928c72b7057 src/HOL/Tools/induct_method.ML --- a/src/HOL/Tools/induct_method.ML Tue Feb 22 21:45:20 2000 +0100 +++ b/src/HOL/Tools/induct_method.ML Tue Feb 22 21:48:24 2000 +0100 @@ -2,7 +2,7 @@ ID: $Id$ Author: Markus Wenzel, TU Muenchen -Proof by induction on types / set / functions. +Proof methods for cases and induction on types / sets / functions. *) signature INDUCT_METHOD = @@ -14,9 +14,110 @@ struct -(* type induct_kind *) +(** utils **) + +(* vars_of *) + +fun vars_of tm = (*ordered left-to-right, preferring right!*) + foldl_aterms (fn (ts, t as Var _) => t :: ts | (ts, _) => ts) ([], tm) + |> Library.distinct |> rev; + + +(* kinds *) + +datatype kind = Type | Set | Function | Rule; + +fun intern_kind Type = Sign.intern_tycon + | intern_kind Set = Sign.intern_const + | intern_kind Function = Sign.intern_const + | intern_kind Rule = K I; (* FIXME !? *) + + + +(** cases method **) + +fun cases_rule Type = DatatypePackage.cases_of o Theory.sign_of + | cases_rule Set = InductivePackage.cases_of o Theory.sign_of + | cases_rule Function = (fn _ => error "No cases rule for recursive functions") + | cases_rule Rule = PureThy.get_thm; + +val cases_var = hd o vars_of o hd o Logic.strip_assums_hyp o Library.last_elem o Thm.prems_of; + + +fun cases_tac (None, None) ctxt = + Method.rule_tac (case_split_thm :: InductivePackage.cases (ProofContext.sign_of ctxt)) + | cases_tac args ctxt = + let + val thy = ProofContext.theory_of ctxt; + val sign = Theory.sign_of thy; + val cert = Thm.cterm_of sign; + + val (kind, name) = + (case args of + (_, Some (kind, bname)) => (kind, intern_kind kind sign bname) + | (Some t, _) => + (case try (#1 o Term.dest_Type o Term.type_of) t of + Some name => (Type, name) + | None => error "Need specific type to figure out cases rule") + | _ => sys_error "cases_tac"); + val rule = cases_rule kind thy name; -datatype induct_kind = Type | Set | Function | Rule; + val inst_rule = + (case #1 args of + None => rule + | Some t => Drule.cterm_instantiate [(cert (cases_var rule), cert t)] rule); + in Method.rule_tac [inst_rule] end; + +val cases_meth = Method.METHOD oo (FINDGOAL ooo cases_tac); + + + +(** induct method **) + +fun induct_rule Type = #induction oo DatatypePackage.datatype_info_err + | induct_rule Set = (#induct o #2) oo InductivePackage.get_inductive + | induct_rule Function = #induct oo RecdefPackage.get_recdef + | induct_rule Rule = PureThy.get_thm; + +fun induct_tac (insts, opt_kind_name) ctxt = + let + val thy = ProofContext.theory_of ctxt; + val sign = Theory.sign_of thy; + val cert = Thm.cterm_of sign; + + val (kind, name) = + (case opt_kind_name of + Some (kind, bname) => (kind, intern_kind kind sign bname) + | None => + (case try (#1 o Term.dest_Type o Term.type_of o Library.last_elem o hd) insts of + Some name => (Type, name) + | None => error "Unable to figure out induction rule")); + val rule = induct_rule kind thy name; + + fun prep_inst (concl, ts) = + let + val xs = vars_of concl; + val n = length xs - length ts; + in + if n < 0 then raise THM ("More arguments given than in induction rule", 0, [rule]) + else map cert (Library.drop (n, xs)) ~~ map cert ts + end; + + val prep_insts = flat o map2 prep_inst; + + val inst_rule = + if null insts then rule + else Drule.cterm_instantiate (prep_insts + (DatatypeAux.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of rule)), insts)) rule; + in Method.rule_tac [inst_rule] end; + +val induct_meth = Method.METHOD oo (FINDGOAL ooo induct_tac); + + + +(** concrete syntax **) + +local val kind_name = Args.$$$ "type" >> K Type || @@ -24,63 +125,32 @@ Args.$$$ "function" >> K Function || Args.$$$ "rule" >> K Rule; -val kind = kind_name --| Args.$$$ ":"; +val kind_spec = kind_name --| Args.$$$ ":"; +val kind = Scan.lift (kind_spec -- Args.name); +val term = Scan.unless (Scan.lift (Scan.option (Args.$$$ "in") -- kind_spec)) Args.local_term; -(* induct_rule *) +fun argument is_empty arg = arg :-- (fn x => + Scan.option (if is_empty x then kind else Scan.lift (Args.$$$ "in") |-- kind)); -fun kind_rule Type = (#induction oo DatatypePackage.datatype_info_err, Sign.intern_tycon) - | kind_rule Set = ((#induct o #2) oo InductivePackage.get_inductive, Sign.intern_const) - | kind_rule Function = (#induct oo RecdefPackage.get_recdef, Sign.intern_const) - | kind_rule Rule = (PureThy.get_thm, K I); +in + +fun cases_args f src ctxt = + f (#2 (Method.syntax (argument is_none (Scan.option term)) src ctxt)) ctxt; -fun induct_rule thy kind name = - let val (ind_rule, intern) = kind_rule kind - in ind_rule thy (intern (Theory.sign_of thy) name) end; +fun induct_args f src ctxt = + f (#2 (Method.syntax (argument null (Args.and_list (Scan.repeat1 term))) src ctxt)) ctxt; + +end; -(* induct_tac *) -fun induct_tac thy insts opt_kind_name facts i state = - let - val (kind, name) = - (case opt_kind_name of Some kind_name => kind_name | None => - (case try (#1 o Term.dest_Type o Term.type_of o #2 o hd) insts of - Some name => (Type, name) - | None => error "Unable to figure out induction rule")); - val rule = Drule.incr_indexes_wrt [] [] [] [state] (induct_rule thy kind name); - - val cert = Thm.cterm_of (Sign.merge (pairself Thm.sign_of_thm (state, rule))); - - fun prep_inst ((P $ x), (Some Q, y)) = [(cert P, cert Q), (cert x, cert y)] - | prep_inst ((_ $ x), (None, y)) = [(cert x, cert y)] - | prep_inst _ = raise THM ("Malformed induction rule", 0, [rule]); - - val prep_insts = flat o map2 prep_inst; +(** theory setup **) - val inst_rule = - if null insts then rule - else Drule.cterm_instantiate (prep_insts - (DatatypeAux.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of rule)), insts)) rule; - in Method.rule_tac [inst_rule] facts i state end; - - -(* induct_method *) - -val term = Scan.unless (Scan.lift kind) Args.local_term; -val inst = term -- term >> (apfst Some) || term >> pair None; - -fun induct ctxt = - Args.and_list inst -- Scan.option (Scan.lift (kind -- Args.name)) - >> (fn (is, k) => Method.METHOD (FINDGOAL o induct_tac (ProofContext.theory_of ctxt) is k)); - -fun induct_meth src ctxt = #2 (Method.syntax (induct ctxt) ctxt src); -val induct_method = ("induct", induct_meth, "induction on types, sets, functions etc."); - - -(* theory setup *) - -val setup = [Method.add_methods [induct_method]]; +val setup = + [Method.add_methods + [("cases", cases_args cases_meth, "case analysis on types / sets"), + ("induct", induct_args induct_meth, "induction on types / sets / functions")]]; end;