src/HOL/Tools/inductive_package.ML
changeset 10729 1b3350c4ee92
parent 10569 e8346dad78e1
child 10735 dfaf75f0076f
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Dec 22 18:24:11 2000 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Dec 22 18:24:39 2000 +0100
     1.3 @@ -60,6 +60,17 @@
     1.4  struct
     1.5  
     1.6  
     1.7 +(** theory context references **)
     1.8 +
     1.9 +val mk_inductive_conj = HOLogic.mk_binop "Inductive.conj";
    1.10 +val inductive_conj_def = thm "conj_def";
    1.11 +val inductive_conj = thms "inductive_conj";
    1.12 +val inductive_atomize = thms "inductive_atomize";
    1.13 +val inductive_rulify1 = thms "inductive_rulify1";
    1.14 +val inductive_rulify2 = thms "inductive_rulify2";
    1.15 +
    1.16 +
    1.17 +
    1.18  (*** theory data ***)
    1.19  
    1.20  (* data kind 'HOL/inductive' *)
    1.21 @@ -218,35 +229,55 @@
    1.22  
    1.23  
    1.24  
    1.25 -(** well-formedness checks **)
    1.26 +(** process rules **)
    1.27 +
    1.28 +local
    1.29  
    1.30 -fun err_in_rule sign t msg = error ("Ill-formed introduction rule\n" ^
    1.31 -  (Sign.string_of_term sign t) ^ "\n" ^ msg);
    1.32 +fun err_in_rule sg name t msg =
    1.33 +  error (cat_lines ["Ill-formed introduction rule " ^ quote name, Sign.string_of_term sg t, msg]);
    1.34 +
    1.35 +fun err_in_prem sg name t p msg =
    1.36 +  error (cat_lines ["Ill-formed premise", Sign.string_of_term sg p,
    1.37 +    "in introduction rule " ^ quote name, Sign.string_of_term sg t, msg]);
    1.38  
    1.39 -fun err_in_prem sign t p msg = error ("Ill-formed premise\n" ^
    1.40 -  (Sign.string_of_term sign p) ^ "\nin introduction rule\n" ^
    1.41 -  (Sign.string_of_term sign t) ^ "\n" ^ msg);
    1.42 +val bad_concl = "Conclusion of introduction rule must have form \"t : S_i\"";
    1.43 +
    1.44 +val atomize_cterm = InductMethod.rewrite_cterm inductive_atomize;
    1.45 +fun full_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);
    1.46 +
    1.47 +in
    1.48  
    1.49 -val msg1 = "Conclusion of introduction rule must have form\
    1.50 -          \ ' t : S_i '";
    1.51 -val msg2 = "Non-atomic premise";
    1.52 -val msg3 = "Recursion term on left of member symbol";
    1.53 +fun check_rule sg cs ((name, rule), att) =
    1.54 +  let
    1.55 +    val concl = Logic.strip_imp_concl rule;
    1.56 +    val prems = Logic.strip_imp_prems rule;
    1.57 +    val aprems = prems |> map (Thm.term_of o atomize_cterm o Thm.cterm_of sg);
    1.58 +    val arule = Logic.list_implies (aprems, concl);
    1.59  
    1.60 -fun check_rule sign cs r =
    1.61 -  let
    1.62 -    fun check_prem prem = if can HOLogic.dest_Trueprop prem then ()
    1.63 -      else err_in_prem sign r prem msg2;
    1.64 +    fun check_prem (prem, aprem) =
    1.65 +      if can HOLogic.dest_Trueprop aprem then ()
    1.66 +      else err_in_prem sg name rule prem "Non-atomic premise";
    1.67 +  in
    1.68 +    (case HOLogic.dest_Trueprop concl of
    1.69 +      (Const ("op :", _) $ t $ u) =>
    1.70 +        if u mem cs then
    1.71 +          if exists (Logic.occs o rpair t) cs then
    1.72 +            err_in_rule sg name rule "Recursion term on left of member symbol"
    1.73 +          else seq check_prem (prems ~~ aprems)
    1.74 +        else err_in_rule sg name rule bad_concl
    1.75 +      | _ => err_in_rule sg name rule bad_concl);
    1.76 +    ((name, arule), att)
    1.77 +  end;
    1.78  
    1.79 -  in (case HOLogic.dest_Trueprop (Logic.strip_imp_concl r) of
    1.80 -        (Const ("op :", _) $ t $ u) =>
    1.81 -          if u mem cs then
    1.82 -            if exists (Logic.occs o (rpair t)) cs then
    1.83 -              err_in_rule sign r msg3
    1.84 -            else
    1.85 -              seq check_prem (Logic.strip_imp_prems r)
    1.86 -          else err_in_rule sign r msg1
    1.87 -      | _ => err_in_rule sign r msg1)
    1.88 -  end;
    1.89 +val rulify =
    1.90 +  standard o full_simplify [Drule.norm_hhf_eq] o
    1.91 +  full_simplify inductive_rulify2 o full_simplify inductive_rulify1 o
    1.92 +  full_simplify inductive_conj;
    1.93 +
    1.94 +fun rulified x = Drule.rule_attribute (K rulify) x;
    1.95 +
    1.96 +end;
    1.97 +
    1.98  
    1.99  fun try' f msg sign t = (case (try f t) of
   1.100        Some x => x
   1.101 @@ -312,7 +343,7 @@
   1.102          fun subst (s as ((m as Const ("op :", T)) $ t $ u)) =
   1.103                (case pred_of u of
   1.104                    None => (m $ fst (subst t) $ fst (subst u), None)
   1.105 -                | Some P => (HOLogic.conj $ s $ (P $ t), Some (s, P $ t)))
   1.106 +                | Some P => (mk_inductive_conj (s, P $ t), Some (s, P $ t)))
   1.107            | subst s =
   1.108                (case pred_of s of
   1.109                    Some P => (HOLogic.mk_binop "op Int"
   1.110 @@ -435,7 +466,8 @@
   1.111         DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 APPEND assume_tac 1),
   1.112         (*Now solve the equations like Inl 0 = Inl ?b2*)
   1.113         rewrite_goals_tac con_defs,
   1.114 -       REPEAT (rtac refl 1)])) (1 upto (length intr_ts) ~~ intr_ts)
   1.115 +       REPEAT (rtac refl 1)])
   1.116 +      |> rulify) (1 upto (length intr_ts) ~~ intr_ts)
   1.117  
   1.118    in (intrs, unfold) end;
   1.119  
   1.120 @@ -459,6 +491,7 @@
   1.121           REPEAT (FIRSTGOAL (eresolve_tac rules2)),
   1.122           EVERY (map (fn prem =>
   1.123             DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])
   1.124 +      |> rulify
   1.125        |> RuleCases.name cases)
   1.126        (mk_elims cs cTs params intr_ts intr_names)
   1.127    end;
   1.128 @@ -572,7 +605,7 @@
   1.129          (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites,
   1.130            rtac refl 1])) cs;
   1.131  
   1.132 -    val induct = prove_goalw_cterm [] (cterm_of sign
   1.133 +    val induct = prove_goalw_cterm [inductive_conj_def] (cterm_of sign
   1.134        (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
   1.135          [rtac (impI RS allI) 1,
   1.136           DETERM (etac (mono RS (fp_def RS def_lfp_induct)) 1),
   1.137 @@ -596,8 +629,7 @@
   1.138              rewrite_goals_tac sum_case_rewrites,
   1.139              atac 1])])
   1.140  
   1.141 -  in standard (split_rule (induct RS lemma))
   1.142 -  end;
   1.143 +  in standard (split_rule (induct RS lemma)) end;
   1.144  
   1.145  
   1.146  
   1.147 @@ -605,6 +637,11 @@
   1.148  
   1.149  (** definitional introduction of (co)inductive sets **)
   1.150  
   1.151 +fun cond_declare_consts declare_consts cs paramTs cnames =
   1.152 +  if declare_consts then
   1.153 +    Theory.add_consts_i (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
   1.154 +  else I;
   1.155 +
   1.156  fun mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
   1.157        params paramTs cTs cnames =
   1.158    let
   1.159 @@ -658,10 +695,7 @@
   1.160  
   1.161      val (thy', [fp_def :: rec_sets_defs]) =
   1.162        thy
   1.163 -      |> (if declare_consts then
   1.164 -          Theory.add_consts_i (map (fn (c, n) =>
   1.165 -            (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
   1.166 -          else I)
   1.167 +      |> cond_declare_consts declare_consts cs paramTs cnames
   1.168        |> (if length cs < 2 then I
   1.169            else Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)])
   1.170        |> Theory.add_path rec_name
   1.171 @@ -706,7 +740,7 @@
   1.172        |> PureThy.add_thmss [(("intros", intrs'), atts)]
   1.173        |>> (if no_elim then I else #1 o PureThy.add_thmss [(("elims", elims), [])])
   1.174        |>> (if no_ind then I else #1 o PureThy.add_thms
   1.175 -        [((coind_prefix coind ^ "induct", induct), [RuleCases.case_names induct_cases])])
   1.176 +        [((coind_prefix coind ^ "induct", rulify induct), [RuleCases.case_names induct_cases])])
   1.177        |>> Theory.parent_path;
   1.178      val elims' = if no_elim then elims else PureThy.get_thms thy3 "elims";  (* FIXME improve *)
   1.179      val induct' = if no_ind then induct else PureThy.get_thm thy3 (coind_prefix coind ^ "induct");  (* FIXME improve *)
   1.180 @@ -717,7 +751,7 @@
   1.181       intrs = intrs'',
   1.182       elims = elims',
   1.183       mk_cases = mk_cases elims',
   1.184 -     raw_induct = raw_induct,
   1.185 +     raw_induct = rulify raw_induct,
   1.186       induct = induct'})
   1.187    end;
   1.188  
   1.189 @@ -740,8 +774,9 @@
   1.190  
   1.191      val (thy2, [intrs, raw_elims]) =
   1.192        thy1
   1.193 -      |> (PureThy.add_axiomss_i o map Thm.no_attributes)
   1.194 -        [("raw_intros", intr_ts), ("raw_elims", elim_ts)]
   1.195 +      |> PureThy.add_axiomss_i
   1.196 +        [(("raw_intros", intr_ts), [rulified]),
   1.197 +          (("raw_elims", elim_ts), [rulified])]
   1.198        |>> (if coind then I else
   1.199              #1 o PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]);
   1.200  
   1.201 @@ -756,7 +791,8 @@
   1.202        thy3
   1.203        |> PureThy.add_thmss [(("intros", intrs'), atts), (("elims", elims), [])]
   1.204        |>> (if coind then I
   1.205 -          else #1 o PureThy.add_thms [(("induct", induct), [RuleCases.case_names induct_cases])])
   1.206 +          else #1 o PureThy.add_thms [(("induct", rulify induct),
   1.207 +            [RuleCases.case_names induct_cases])])
   1.208        |>> Theory.parent_path;
   1.209      val induct' = if coind then raw_induct else PureThy.get_thm thy4 "induct";
   1.210    in (thy4,
   1.211 @@ -766,7 +802,7 @@
   1.212       intrs = intrs'',
   1.213       elims = elims',
   1.214       mk_cases = mk_cases elims',
   1.215 -     raw_induct = raw_induct,
   1.216 +     raw_induct = rulify raw_induct,
   1.217       induct = induct'})
   1.218    end;
   1.219  
   1.220 @@ -775,7 +811,7 @@
   1.221  (** introduction of (co)inductive sets **)
   1.222  
   1.223  fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
   1.224 -    atts intros monos con_defs thy =
   1.225 +    atts pre_intros monos con_defs thy =
   1.226    let
   1.227      val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
   1.228      val sign = Theory.sign_of thy;
   1.229 @@ -792,7 +828,9 @@
   1.230        "Recursive set not previously declared as constant: " sign) cs;
   1.231      val cnames = map Sign.base_name full_cnames;
   1.232  
   1.233 -    val _ = seq (check_rule sign cs o snd o fst) intros;
   1.234 +    val save_sign =
   1.235 +      thy |> Theory.copy |> cond_declare_consts declare_consts cs paramTs cnames |> Theory.sign_of;
   1.236 +    val intros = map (check_rule save_sign cs) pre_intros;
   1.237      val induct_cases = map (#1 o #1) intros;
   1.238  
   1.239      val (thy1, result as {elims, induct, ...}) =