1.1 --- a/src/HOL/BNF/Tools/coinduction.ML Thu Dec 05 17:52:12 2013 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,159 +0,0 @@
1.4 -(* Title: HOL/BNF/Tools/coinduction.ML
1.5 - Author: Johannes Hölzl, TU Muenchen
1.6 - Author: Dmitriy Traytel, TU Muenchen
1.7 - Copyright 2013
1.8 -
1.9 -Coinduction method that avoids some boilerplate compared to coinduct.
1.10 -*)
1.11 -
1.12 -signature COINDUCTION =
1.13 -sig
1.14 - val coinduction_tac: Proof.context -> term list -> thm option -> thm list -> cases_tactic
1.15 - val setup: theory -> theory
1.16 -end;
1.17 -
1.18 -structure Coinduction : COINDUCTION =
1.19 -struct
1.20 -
1.21 -open BNF_Util
1.22 -open BNF_Tactics
1.23 -
1.24 -fun filter_in_out _ [] = ([], [])
1.25 - | filter_in_out P (x :: xs) = (let
1.26 - val (ins, outs) = filter_in_out P xs;
1.27 - in
1.28 - if P x then (x :: ins, outs) else (ins, x :: outs)
1.29 - end);
1.30 -
1.31 -fun ALLGOALS_SKIP skip tac st =
1.32 - let fun doall n = if n = skip then all_tac else tac n THEN doall (n - 1)
1.33 - in doall (nprems_of st) st end;
1.34 -
1.35 -fun THEN_ALL_NEW_SKIP skip tac1 tac2 i st =
1.36 - st |> (tac1 i THEN (fn st' =>
1.37 - Seq.INTERVAL tac2 (i + skip) (i + nprems_of st' - nprems_of st) st'));
1.38 -
1.39 -fun DELETE_PREMS_AFTER skip tac i st =
1.40 - let
1.41 - val n = nth (prems_of st) (i - 1) |> Logic.strip_assums_hyp |> length;
1.42 - in
1.43 - (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o etac thin_rl)) i st
1.44 - end;
1.45 -
1.46 -fun coinduction_tac ctxt raw_vars opt_raw_thm prems st =
1.47 - let
1.48 - val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
1.49 - fun find_coinduct t =
1.50 - Induct.find_coinductP ctxt t @
1.51 - (try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default [])
1.52 - val raw_thm = case opt_raw_thm
1.53 - of SOME raw_thm => raw_thm
1.54 - | NONE => st |> prems_of |> hd |> Logic.strip_assums_concl |> find_coinduct |> hd;
1.55 - val skip = Integer.max 1 (Rule_Cases.get_consumes raw_thm) - 1
1.56 - val cases = Rule_Cases.get raw_thm |> fst
1.57 - in
1.58 - NO_CASES (HEADGOAL (
1.59 - Object_Logic.rulify_tac THEN'
1.60 - Method.insert_tac prems THEN'
1.61 - Object_Logic.atomize_prems_tac THEN'
1.62 - DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} =>
1.63 - let
1.64 - val vars = raw_vars @ map (term_of o snd) params;
1.65 - val names_ctxt = ctxt
1.66 - |> fold Variable.declare_names vars
1.67 - |> fold Variable.declare_thm (raw_thm :: prems);
1.68 - val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
1.69 - val (rhoTs, rhots) = Thm.match (thm_concl, concl)
1.70 - |>> map (pairself typ_of)
1.71 - ||> map (pairself term_of);
1.72 - val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
1.73 - |> map (subst_atomic_types rhoTs);
1.74 - val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
1.75 - val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
1.76 - |>> (fn names => Variable.variant_fixes names names_ctxt) ;
1.77 - val eqs =
1.78 - map3 (fn name => fn T => fn (_, rhs) =>
1.79 - HOLogic.mk_eq (Free (name, T), rhs))
1.80 - names Ts raw_eqs;
1.81 - val phi = eqs @ map (HOLogic.dest_Trueprop o prop_of) prems
1.82 - |> try (Library.foldr1 HOLogic.mk_conj)
1.83 - |> the_default @{term True}
1.84 - |> list_exists_free vars
1.85 - |> Term.map_abs_vars (Variable.revert_fixed ctxt)
1.86 - |> fold_rev Term.absfree (names ~~ Ts)
1.87 - |> certify ctxt;
1.88 - val thm = cterm_instantiate_pos [SOME phi] raw_thm;
1.89 - val e = length eqs;
1.90 - val p = length prems;
1.91 - in
1.92 - HEADGOAL (EVERY' [rtac thm,
1.93 - EVERY' (map (fn var =>
1.94 - rtac (cterm_instantiate_pos [NONE, SOME (certify ctxt var)] exI)) vars),
1.95 - if p = 0 then CONJ_WRAP' (K (rtac refl)) eqs
1.96 - else REPEAT_DETERM_N e o (rtac conjI THEN' rtac refl) THEN' CONJ_WRAP' rtac prems,
1.97 - K (ALLGOALS_SKIP skip
1.98 - (REPEAT_DETERM_N (length vars) o (etac exE THEN' rotate_tac ~1) THEN'
1.99 - DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
1.100 - (case prems of
1.101 - [] => all_tac
1.102 - | inv::case_prems =>
1.103 - let
1.104 - val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv;
1.105 - val inv_thms = init @ [last];
1.106 - val eqs = take e inv_thms;
1.107 - fun is_local_var t =
1.108 - member (fn (t, (_, t')) => t aconv (term_of t')) params t;
1.109 - val (eqs, assms') = filter_in_out (is_local_var o lhs_of_eq o prop_of) eqs;
1.110 - val assms = assms' @ drop e inv_thms
1.111 - in
1.112 - HEADGOAL (Method.insert_tac (assms @ case_prems)) THEN
1.113 - unfold_thms_tac ctxt eqs
1.114 - end)) ctxt)))])
1.115 - end) ctxt) THEN'
1.116 - K (prune_params_tac))) st
1.117 - |> Seq.maps (fn (_, st) =>
1.118 - CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, prop_of st) cases) all_tac st)
1.119 - end;
1.120 -
1.121 -local
1.122 -
1.123 -val ruleN = "rule"
1.124 -val arbitraryN = "arbitrary"
1.125 -fun single_rule [rule] = rule
1.126 - | single_rule _ = error "Single rule expected";
1.127 -
1.128 -fun named_rule k arg get =
1.129 - Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :|--
1.130 - (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name =>
1.131 - (case get (Context.proof_of context) name of SOME x => x
1.132 - | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
1.133 -
1.134 -fun rule get_type get_pred =
1.135 - named_rule Induct.typeN (Args.type_name false) get_type ||
1.136 - named_rule Induct.predN (Args.const false) get_pred ||
1.137 - named_rule Induct.setN (Args.const false) get_pred ||
1.138 - Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
1.139 -
1.140 -val coinduct_rule = rule Induct.lookup_coinductT Induct.lookup_coinductP >> single_rule;
1.141 -
1.142 -fun unless_more_args scan = Scan.unless (Scan.lift
1.143 - ((Args.$$$ arbitraryN || Args.$$$ Induct.typeN ||
1.144 - Args.$$$ Induct.predN || Args.$$$ Induct.setN || Args.$$$ ruleN) -- Args.colon)) scan;
1.145 -
1.146 -val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
1.147 - Scan.repeat1 (unless_more_args Args.term)) [];
1.148 -
1.149 -in
1.150 -
1.151 -val setup =
1.152 - Method.setup @{binding coinduction}
1.153 - (arbitrary -- Scan.option coinduct_rule >>
1.154 - (fn (arbitrary, opt_rule) => fn ctxt =>
1.155 - RAW_METHOD_CASES (fn facts =>
1.156 - Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts))))
1.157 - "coinduction on types or predicates/sets";
1.158 -
1.159 -end;
1.160 -
1.161 -end;
1.162 -