reworked version with proper support for defs, fixes, fresh specification;
authorwenzelm
Tue Nov 29 18:09:12 2005 +0100 (2005-11-29)
changeset 18283f8a49f09a202
parent 18282 98431741bda3
child 18284 cd217d16c90d
reworked version with proper support for defs, fixes, fresh specification;
src/HOL/Nominal/nominal_induct.ML
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Tue Nov 29 16:05:10 2005 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Tue Nov 29 18:09:12 2005 +0100
     1.3 @@ -1,87 +1,143 @@
     1.4 -(* $Id$ *)
     1.5 +(*  ID:         $Id$
     1.6 +    Author:     Christian Urban
     1.7 +
     1.8 +The nominal induct proof method (cf. ~~/src/Provers/induct_method.ML).
     1.9 +*)
    1.10 +
    1.11 +structure NominalInduct:
    1.12 +sig
    1.13 +  val nominal_induct_tac: Proof.context -> (string option * term) option list ->
    1.14 +    term list -> (string * typ) list list -> thm -> thm list -> int -> RuleCases.cases_tactic
    1.15 +  val nominal_induct_method: Method.src -> Proof.context -> Method.method
    1.16 +end =
    1.17 +struct
    1.18 +
    1.19 +
    1.20 +(** misc tools **)
    1.21 +
    1.22 +fun nth_list xss i = nth xss i handle Subscript => [];
    1.23 +
    1.24 +fun align_right msg xs ys =
    1.25 +  let val m = length xs and n = length ys
    1.26 +  in if m < n then raise ERROR_MESSAGE msg else (Library.drop (m - n, xs) ~~ ys) end;
    1.27 +
    1.28 +fun prep_inst thy tune (tm, ts) =
    1.29 +  let
    1.30 +    val cert = Thm.cterm_of thy;
    1.31 +    fun prep_var (x, SOME t) =
    1.32 +          let
    1.33 +            val cx = cert x;
    1.34 +            val {T = xT, thy, ...} = Thm.rep_cterm cx;
    1.35 +            val ct = cert (tune t);
    1.36 +          in
    1.37 +            if Sign.typ_instance thy (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct)
    1.38 +            else raise ERROR_MESSAGE (Pretty.string_of (Pretty.block
    1.39 +             [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
    1.40 +              Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
    1.41 +              Display.pretty_ctyp (#T (Thm.crep_cterm ct))]))
    1.42 +          end
    1.43 +      | prep_var (_, NONE) = NONE;
    1.44 +    val xs = InductAttrib.vars_of tm;
    1.45 +  in
    1.46 +    align_right "Rule has fewer variables than instantiations given" xs ts
    1.47 +    |> List.mapPartial prep_var
    1.48 +  end;
    1.49 +
    1.50 +fun add_defs def_insts =
    1.51 +  let
    1.52 +    fun add (SOME (SOME x, t)) ctxt =
    1.53 +          let val ((lhs, def), ctxt') = ProofContext.add_def (x, t) ctxt
    1.54 +          in ((SOME (Free lhs), [def]), ctxt') end
    1.55 +      | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
    1.56 +      | add NONE ctxt = ((NONE, []), ctxt);
    1.57 +  in fold_map add def_insts #> apfst (split_list #> apsnd List.concat) end;
    1.58 +
    1.59 +
    1.60 +
    1.61 +(** nominal_induct_tac **)
    1.62 +
    1.63 +fun make_fresh [] = HOLogic.unit
    1.64 +  | make_fresh [t] = t
    1.65 +  | make_fresh ts = foldr1 HOLogic.mk_prod ts;
    1.66 +
    1.67 +val split_fresh =
    1.68 +  Simplifier.full_simplify (HOL_basic_ss addsimps [split_paired_all, unit_all_eq1]);
    1.69 +
    1.70 +fun nominal_induct_tac ctxt def_insts fresh fixing rule facts =
    1.71 +  let
    1.72 +    val thy = ProofContext.theory_of ctxt;
    1.73 +    val cert = Thm.cterm_of thy;
    1.74 +
    1.75 +    val ((insts, defs), defs_ctxt) = add_defs def_insts ctxt;
    1.76 +    val atomized_defs = map ObjectLogic.atomize_thm defs;
    1.77 +
    1.78 +    fun inst_rule r =
    1.79 +      Drule.cterm_instantiate
    1.80 +        (prep_inst thy (InductMethod.atomize_term thy)
    1.81 +          (Thm.concl_of r, insts @ [SOME (make_fresh fresh)])) r;
    1.82 +
    1.83 +    fun rule_cases r = RuleCases.make false (SOME (Thm.prop_of r)) (InductMethod.rulified_term r);
    1.84 +  in
    1.85 +    SUBGOAL_CASES (fn (goal, i) => fn st =>
    1.86 +      rule
    1.87 +      |> inst_rule
    1.88 +      |> `RuleCases.get
    1.89 +      |> RuleCases.consume defs facts
    1.90 +      |> Seq.maps (fn ((cases, (k, more_facts)), r) =>
    1.91 +        (CONJUNCTS (ALLGOALS (fn j =>
    1.92 +            Method.insert_tac (more_facts @ atomized_defs) j
    1.93 +            THEN InductMethod.fix_tac defs_ctxt k (nth_list fixing (j - 1)) j))
    1.94 +          THEN' InductMethod.atomize_tac) i st |> Seq.maps (fn st' =>
    1.95 +            InductMethod.guess_instance (split_fresh r) i st'
    1.96 +            |> Seq.maps (fn r' =>
    1.97 +              CASES (rule_cases r' cases)
    1.98 +                (Tactic.rtac r' i THEN
    1.99 +                  PRIMSEQ (ProofContext.exports defs_ctxt ctxt)) st'))))
   1.100 +    THEN_ALL_NEW_CASES InductMethod.rulify_tac
   1.101 +  end;
   1.102 +
   1.103 +
   1.104 +
   1.105 +(** concrete syntax **)
   1.106  
   1.107  local
   1.108  
   1.109 -(* A function that takes a list of Variables and a term t;                    *)
   1.110 -(* it builds up an abstraction of the Variables packaged in a tuple(!)        *)
   1.111 -(* over the term t.                                                           *)
   1.112 -(* E.g  tuple_lambda [] t        produces %x . t where x is a dummy Variable  *) 
   1.113 -(*      tuple_lambda [a] t       produces %a . t                              *) 
   1.114 -(*      tuple_lambda [a,b,c] t   produces %(a,b,c). t                         *)
   1.115 +val freshN = "fresh";
   1.116 +val fixingN = "fixing";
   1.117 +val ruleN = "rule";
   1.118  
   1.119 -fun tuple_lambda [] t  = Abs ("x", HOLogic.unitT, t)
   1.120 -  | tuple_lambda [x] t = lambda x t
   1.121 -  | tuple_lambda (x::xs) t =
   1.122 -    let
   1.123 -        val t' = tuple_lambda xs t;
   1.124 -        val Type ("fun", [T,U]) = fastype_of t';
   1.125 -    in
   1.126 -        HOLogic.split_const (fastype_of x,T,U) $ lambda x t'
   1.127 -    end; 
   1.128 +val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.local_term >> SOME;
   1.129  
   1.130 -fun find_var frees name =
   1.131 -  (case Library.find_first (equal name o fst o dest_Free) frees of
   1.132 -    NONE =>   error ("No such Variable in term: " ^ quote name) 
   1.133 -  | SOME v => v);
   1.134 -
   1.135 -(* - names specifies the variables that are involved in the *)
   1.136 -(*   induction                                              *)
   1.137 -(* - rule is the induction rule to be applied               *)              
   1.138 -fun nominal_induct_tac (names, rule) facts state =
   1.139 -  let
   1.140 -    val sg     = Thm.sign_of_thm state;
   1.141 -    val cert   = Thm.cterm_of sg;
   1.142 -
   1.143 -    val facts1 = Library.take (1, facts);
   1.144 -    val facts2 = Library.drop (1, facts);
   1.145 +val def_inst =
   1.146 +  ((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME)
   1.147 +      -- Args.local_term) >> SOME ||
   1.148 +    inst >> Option.map (pair NONE);
   1.149  
   1.150 -    val goal :: _ = Thm.prems_of state;  (*exception Subscript*)
   1.151 -    val frees  = foldl Term.add_term_frees [] (goal :: map concl_of facts1);
   1.152 -    val frees' = filter_out (fn Free (x, _) => exists (equal x) names) frees;
   1.153 -    val vars = map (find_var frees) names; 
   1.154 -                 (* FIXME - check what one can do in case of *)
   1.155 -                 (* rule inductions                          *)
   1.156 +val free = Scan.state -- Args.local_term >> (fn (_, Free v) => v | (ctxt, t) =>
   1.157 +  error ("Bad free variable: " ^ ProofContext.string_of_term ctxt t));
   1.158 +
   1.159 +fun unless_more_args scan = Scan.unless (Scan.lift
   1.160 +  ((Args.$$$ freshN || Args.$$$ fixingN || Args.$$$ ruleN) -- Args.colon)) scan;
   1.161 +
   1.162  
   1.163 -    fun inst_rule rule =
   1.164 -      let
   1.165 -        val concl_vars = map Var (rev (Term.add_vars (Thm.concl_of rule) []));
   1.166 -        val (P :: ts, x) = split_last concl_vars
   1.167 -          handle Empty => error "Malformed conclusion of induction rule"
   1.168 -               | Bind  => error "Malformed conclusion of induction rule";
   1.169 -      in
   1.170 -        cterm_instantiate
   1.171 -          ((cert P, cert (fold_rev lambda vars (tuple_lambda frees' (HOLogic.dest_Trueprop goal)))) ::
   1.172 -           (cert x, cert (if null frees' then HOLogic.unit else foldr1 HOLogic.mk_prod frees')) ::
   1.173 -           (map cert ts ~~ map cert vars)) rule
   1.174 -      end;
   1.175 +val def_insts = Scan.repeat (unless_more_args def_inst);
   1.176  
   1.177 -    val simplify_rule =
   1.178 -      Simplifier.full_simplify (HOL_basic_ss addsimps
   1.179 -        simp_thms @ [triv_forall_equality, split_conv, split_paired_All, split_paired_all]);
   1.180 +val fresh = Scan.optional (Scan.lift (Args.$$$ freshN -- Args.colon) |--
   1.181 +  Scan.repeat (unless_more_args Args.local_term)) [];
   1.182  
   1.183 -  in
   1.184 -    rule
   1.185 -    |> inst_rule
   1.186 -    |> Method.multi_resolve facts1
   1.187 -    |> Seq.map simplify_rule 
   1.188 -    |> Seq.map (RuleCases.save rule)
   1.189 -    |> Seq.map RuleCases.add
   1.190 -    |> Seq.map (fn (r, (cases, _)) =>
   1.191 -        HEADGOAL (Method.insert_tac facts2 THEN' Tactic.rtac r) state
   1.192 -        |> Seq.map (rpair (RuleCases.make false NONE (sg, Thm.prop_of r) cases)))
   1.193 -    |> Seq.flat
   1.194 -  end
   1.195 -  handle Subscript => Seq.empty;
   1.196 +val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |--
   1.197 +  Args.and_list1 (Scan.repeat (unless_more_args free))) [];
   1.198  
   1.199  val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.local_thm;
   1.200  
   1.201 -val nominal_induct_args =
   1.202 -  Scan.repeat (Scan.unless rule_spec (Scan.lift Args.name)) -- rule_spec;
   1.203 -
   1.204  in
   1.205  
   1.206 -val nominal_induct_method =
   1.207 -  Method.RAW_METHOD_CASES o nominal_induct_tac oo (#2 oo Method.syntax nominal_induct_args);
   1.208 -
   1.209 +fun nominal_induct_method src =
   1.210 +  Method.syntax (def_insts -- fresh -- fixing -- rule_spec) src
   1.211 +  #> (fn (ctxt, (((x, y), z), w)) =>
   1.212 +    Method.RAW_METHOD_CASES (fn facts =>
   1.213 +      HEADGOAL (nominal_induct_tac ctxt x y z w facts)));
   1.214  
   1.215  end;
   1.216 +
   1.217 +end;