Restructured and repaired code dealing with case names
authorberghofe
Tue Oct 17 09:51:04 2006 +0200 (2006-10-17)
changeset 21048e57e91f72831
parent 21047 0cf1800ff7cf
child 21049 379542c9d951
Restructured and repaired code dealing with case names
in induction and elimination rules.
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Oct 17 02:40:21 2006 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Oct 17 09:51:04 2006 +0200
     1.3 @@ -277,37 +277,6 @@
     1.4  
     1.5  
     1.6  
     1.7 -(** properties of (co)inductive predicates **)
     1.8 -
     1.9 -(* prepare cases and induct rules *)
    1.10 -
    1.11 -fun add_cases_induct no_elim no_induct coind rec_name names elims induct =
    1.12 -  let
    1.13 -    fun cases_spec name elim =
    1.14 -      LocalTheory.note ((NameSpace.append (Sign.base_name name) "cases",
    1.15 -        [Attrib.internal (InductAttrib.cases_set name)]), [elim]) #> snd;
    1.16 -    val cases_specs = if no_elim then [] else map2 cases_spec names elims;
    1.17 -
    1.18 -    val induct_att = if coind then InductAttrib.coinduct_set else InductAttrib.induct_set;
    1.19 -    fun induct_specs ctxt =
    1.20 -      if no_induct then ctxt
    1.21 -      else
    1.22 -        let
    1.23 -          val rules = names ~~ ProjectRule.projects ctxt (1 upto length names) induct;
    1.24 -          val inducts = map (RuleCases.save induct o standard o #2) rules;
    1.25 -        in
    1.26 -          ctxt |>
    1.27 -          LocalTheory.notes (rules |> map (fn (name, th) =>
    1.28 -            (("", [Attrib.internal (RuleCases.consumes 1),
    1.29 -                Attrib.internal (induct_att name)]), [([th], [])]))) |> snd |>
    1.30 -          LocalTheory.note ((NameSpace.append rec_name
    1.31 -              (coind_prefix coind ^ "inducts"),
    1.32 -            [Attrib.internal (RuleCases.consumes 1)]), inducts) |> snd
    1.33 -        end;
    1.34 -  in Library.apply cases_specs #> induct_specs end;
    1.35 -
    1.36 -
    1.37 -
    1.38  (** proofs for (co)inductive predicates **)
    1.39  
    1.40  (* prove monotonicity -- NOT subject to quick_and_dirty! *)
    1.41 @@ -386,7 +355,7 @@
    1.42          val prems = HOLogic.mk_Trueprop (list_comb (c, params @ frees)) ::
    1.43             map mk_elim_prem (map #1 c_intrs)
    1.44        in
    1.45 -        SkipProof.prove ctxt'' [] prems P
    1.46 +        (SkipProof.prove ctxt'' [] prems P
    1.47            (fn {prems, ...} => EVERY
    1.48              [cut_facts_tac [hd prems] 1,
    1.49               rewrite_goals_tac rec_preds_defs,
    1.50 @@ -396,8 +365,8 @@
    1.51               EVERY (map (fn prem =>
    1.52                 DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))])
    1.53            |> rulify
    1.54 -          |> singleton (ProofContext.export ctxt'' ctxt)
    1.55 -          |> RuleCases.name (map #2 c_intrs)
    1.56 +          |> singleton (ProofContext.export ctxt'' ctxt),
    1.57 +         map #2 c_intrs)
    1.58        end
    1.59  
    1.60     in map prove_elim cs end;
    1.61 @@ -620,14 +589,14 @@
    1.62      fun transform_rule r =
    1.63        let
    1.64          val SOME (_, i, ts, (Ts, _)) = dest_predicate cs params
    1.65 -          (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))
    1.66 -
    1.67 +          (HOLogic.dest_Trueprop (Logic.strip_assums_concl r));
    1.68 +        val ps = make_bool_args HOLogic.mk_not I bs i @
    1.69 +          map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @
    1.70 +          map (subst o HOLogic.dest_Trueprop)
    1.71 +            (Logic.strip_assums_hyp r)
    1.72        in foldr (fn ((x, T), P) => HOLogic.exists_const T $ (Abs (x, T, P)))
    1.73 -        (foldr1 HOLogic.mk_conj
    1.74 -          (make_bool_args HOLogic.mk_not I bs i @
    1.75 -           map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @
    1.76 -           map (subst o HOLogic.dest_Trueprop)
    1.77 -             (Logic.strip_assums_hyp r))) (Logic.strip_params r)
    1.78 +        (if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps)
    1.79 +        (Logic.strip_params r)
    1.80        end
    1.81  
    1.82      (* make a disjunction of all introduction rules *)
    1.83 @@ -671,12 +640,13 @@
    1.84    end;
    1.85  
    1.86  fun add_ind_def verbose alt_name coind no_elim no_ind cs
    1.87 -    intros monos params cnames_syn induct_cases ctxt =
    1.88 +    intros monos params cnames_syn ctxt =
    1.89    let
    1.90      val _ =
    1.91        if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^
    1.92          commas_quote (map fst cnames_syn)) else ();
    1.93  
    1.94 +    val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o #1) cnames_syn;
    1.95      val ((intr_names, intr_atts), intr_ts) = apfst split_list (split_list intros);
    1.96  
    1.97      val (ctxt1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
    1.98 @@ -685,8 +655,9 @@
    1.99  
   1.100      val (intrs, unfold) = prove_intrs coind mono fp_def (length bs + length xs)
   1.101        intr_ts rec_preds_defs ctxt1;
   1.102 -    val elims = ProofContext.export ctxt1 ctxt (if no_elim then [] else
   1.103 -      prove_elims cs params intr_ts intr_names unfold rec_preds_defs ctxt1);
   1.104 +    val elims = if no_elim then [] else
   1.105 +      cnames ~~ map (apfst (singleton (ProofContext.export ctxt1 ctxt)))
   1.106 +        (prove_elims cs params intr_ts intr_names unfold rec_preds_defs ctxt1);
   1.107      val raw_induct = singleton (ProofContext.export ctxt1 ctxt)
   1.108        (if no_ind then Drule.asm_rl else
   1.109         if coind then ObjectLogic.rulify (rule_by_tactic
   1.110 @@ -695,37 +666,65 @@
   1.111         else
   1.112           prove_indrule cs argTs bs xs rec_const params intr_ts mono fp_def
   1.113             rec_preds_defs ctxt1);
   1.114 +    val induct_cases = map (#1 o #1) intros;
   1.115 +    val ind_case_names = RuleCases.case_names induct_cases;
   1.116      val induct =
   1.117        if coind then
   1.118          (raw_induct, [RuleCases.case_names [rec_name],
   1.119            RuleCases.case_conclusion (rec_name, induct_cases),
   1.120            RuleCases.consumes 1])
   1.121        else if no_ind orelse length cs > 1 then
   1.122 -        (raw_induct, [RuleCases.case_names induct_cases, RuleCases.consumes 0])
   1.123 -      else (raw_induct RSN (2, rev_mp), [RuleCases.case_names induct_cases, RuleCases.consumes 1]);
   1.124 +        (raw_induct, [ind_case_names, RuleCases.consumes 0])
   1.125 +      else (raw_induct RSN (2, rev_mp), [ind_case_names, RuleCases.consumes 1]);
   1.126  
   1.127      val (intrs', ctxt2) =
   1.128        ctxt1 |>
   1.129 -      LocalTheory.notes (map (NameSpace.append rec_name) intr_names ~~ intr_atts ~~
   1.130 -        map (single o rpair [] o single) (ProofContext.export ctxt1 ctxt intrs)) |>>
   1.131 +      LocalTheory.notes
   1.132 +        (map (fn "" => "" | name => NameSpace.append rec_name name) intr_names ~~
   1.133 +         intr_atts ~~
   1.134 +         map (single o rpair [] o single) (ProofContext.export ctxt1 ctxt intrs)) |>>
   1.135        map (hd o snd); (* FIXME? *)
   1.136 -    val (((_, (_, elims')), (_, [induct'])), ctxt3) =
   1.137 +    val (((_, elims'), (_, [induct'])), ctxt3) =
   1.138        ctxt2 |>
   1.139        LocalTheory.note ((NameSpace.append rec_name "intros", []), intrs') ||>>
   1.140 -      LocalTheory.note ((NameSpace.append rec_name "elims",
   1.141 -        [Attrib.internal (RuleCases.consumes 1)]), elims) ||>>
   1.142 +      fold_map (fn (name, (elim, cases)) =>
   1.143 +        LocalTheory.note ((NameSpace.append (Sign.base_name name) "cases",
   1.144 +          [Attrib.internal (RuleCases.case_names cases),
   1.145 +           Attrib.internal (RuleCases.consumes 1),
   1.146 +           Attrib.internal (InductAttrib.cases_set name)]), [elim]) #>
   1.147 +        apfst (hd o snd)) elims ||>>
   1.148        LocalTheory.note ((NameSpace.append rec_name (coind_prefix coind ^ "induct"),
   1.149 -        map Attrib.internal (#2 induct)), [rulify (#1 induct)])
   1.150 -  in (ctxt3, rec_name,
   1.151 -    {preds = preds,
   1.152 -     defs = fp_def :: rec_preds_defs,
   1.153 -     mono = singleton (ProofContext.export ctxt1 ctxt) mono,
   1.154 -     unfold = singleton (ProofContext.export ctxt1 ctxt) unfold,
   1.155 -     intrs = intrs',
   1.156 -     elims = elims',
   1.157 -     mk_cases = mk_cases elims',
   1.158 -     raw_induct = rulify raw_induct,
   1.159 -     induct = induct'})
   1.160 +        map Attrib.internal (#2 induct)), [rulify (#1 induct)]);
   1.161 +
   1.162 +    val induct_att = if coind then InductAttrib.coinduct_set else InductAttrib.induct_set;
   1.163 +    val ctxt4 = if no_ind then ctxt3 else
   1.164 +      let val inducts = cnames ~~ ProjectRule.projects ctxt (1 upto length cnames) induct'
   1.165 +      in
   1.166 +        ctxt3 |>
   1.167 +        LocalTheory.notes (inducts |> map (fn (name, th) => (("",
   1.168 +          [Attrib.internal ind_case_names,
   1.169 +           Attrib.internal (RuleCases.consumes 1),
   1.170 +           Attrib.internal (induct_att name)]), [([th], [])]))) |> snd |>
   1.171 +        LocalTheory.note ((NameSpace.append rec_name (coind_prefix coind ^ "inducts"),
   1.172 +          [Attrib.internal ind_case_names,
   1.173 +           Attrib.internal (RuleCases.consumes 1)]), map snd inducts) |> snd
   1.174 +      end;
   1.175 +
   1.176 +    val result =
   1.177 +      {preds = preds,
   1.178 +       defs = fp_def :: rec_preds_defs,
   1.179 +       mono = singleton (ProofContext.export ctxt1 ctxt) mono,
   1.180 +       unfold = singleton (ProofContext.export ctxt1 ctxt) unfold,
   1.181 +       intrs = intrs',
   1.182 +       elims = elims',
   1.183 +       mk_cases = mk_cases elims',
   1.184 +       raw_induct = rulify raw_induct,
   1.185 +       induct = induct'}
   1.186 +      
   1.187 +  in
   1.188 +    (LocalTheory.declaration
   1.189 +       (put_inductives cnames ({names = cnames, coind = coind}, result)) ctxt4,
   1.190 +     result)
   1.191    end;
   1.192  
   1.193  
   1.194 @@ -745,7 +744,6 @@
   1.195      val cs = map
   1.196        (fn (s, SOME T, _) => Free (s, T) | (s, NONE, _) => Free (s, type_of s)) cnames_syn;
   1.197      val cnames_syn' = map (fn (s, _, mx) => (s, mx)) cnames_syn;
   1.198 -    val cnames = map (Sign.full_name thy o #1) cnames_syn;
   1.199  
   1.200      fun close_rule (x, r) = (x, list_all_free (rev (fold_aterms
   1.201        (fn t as Free (v as (s, _)) =>
   1.202 @@ -754,16 +752,10 @@
   1.203          | _ => I) r []), r));
   1.204  
   1.205      val intros = map (close_rule o check_rule thy cs params) pre_intros;
   1.206 -    val induct_cases = map (#1 o #1) intros;
   1.207 -
   1.208 -    val (ctxt1, rec_name, result as {elims, induct, ...}) =
   1.209 -      add_ind_def verbose alt_name coind no_elim no_ind cs intros monos
   1.210 -        params cnames_syn' induct_cases ctxt;
   1.211 -    val ctxt2 = ctxt1
   1.212 -      |> LocalTheory.declaration
   1.213 -        (put_inductives cnames ({names = cnames, coind = coind}, result))
   1.214 -      |> add_cases_induct no_elim no_ind coind rec_name cnames elims induct;
   1.215 -  in (ctxt2, result) end;
   1.216 +  in
   1.217 +    add_ind_def verbose alt_name coind no_elim no_ind cs intros monos
   1.218 +      params cnames_syn' ctxt
   1.219 +  end;
   1.220  
   1.221  fun add_inductive verbose coind cnames_syn pnames_syn intro_srcs raw_monos ctxt =
   1.222    let