src/HOL/Tools/inductive_realizer.ML
changeset 37236 739d8b9c59da
parent 37136 e0c9d3e49e15
parent 37233 b78f31ca4675
child 37678 0040bafffdef
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Jun 01 11:18:51 2010 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jun 01 11:30:57 2010 +0200
     1.3 @@ -21,18 +21,12 @@
     1.4      [name] => name
     1.5    | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
     1.6  
     1.7 -val all_simps = map (Thm.symmetric o mk_meta_eq) @{thms HOL.all_simps};
     1.8 -
     1.9  fun prf_of thm =
    1.10    let
    1.11      val thy = Thm.theory_of_thm thm;
    1.12      val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
    1.13    in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
    1.14  
    1.15 -fun forall_intr_prf t prf =
    1.16 -  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    1.17 -  in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
    1.18 -
    1.19  fun subsets [] = [[]]
    1.20    | subsets (x::xs) =
    1.21        let val ys = subsets xs
    1.22 @@ -55,15 +49,19 @@
    1.23        (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
    1.24    | strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q);
    1.25  
    1.26 -fun relevant_vars prop = List.foldr (fn
    1.27 -      (Var ((a, i), T), vs) => (case strip_type T of
    1.28 +fun relevant_vars prop = fold (fn ((a, i), T) => fn vs =>
    1.29 +     (case strip_type T of
    1.30          (_, Type (s, _)) => if s = @{type_name bool} then (a, T) :: vs else vs
    1.31 -      | _ => vs)
    1.32 -    | (_, vs) => vs) [] (OldTerm.term_vars prop);
    1.33 +      | _ => vs)) (Term.add_vars prop []) [];
    1.34 +
    1.35 +val attach_typeS = map_types (map_atyps
    1.36 +  (fn TFree (s, []) => TFree (s, HOLogic.typeS)
    1.37 +    | TVar (ixn, []) => TVar (ixn, HOLogic.typeS)
    1.38 +    | T => T));
    1.39  
    1.40  fun dt_of_intrs thy vs nparms intrs =
    1.41    let
    1.42 -    val iTs = OldTerm.term_tvars (prop_of (hd intrs));
    1.43 +    val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []);
    1.44      val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
    1.45        (Logic.strip_imp_concl (prop_of (hd intrs))));
    1.46      val params = map dest_Var (take nparms ts);
    1.47 @@ -84,7 +82,7 @@
    1.48  fun gen_rvar vs (t as Var ((a, 0), T)) =
    1.49        if body_type T <> HOLogic.boolT then t else
    1.50          let
    1.51 -          val U = TVar (("'" ^ a, 0), HOLogic.typeS)
    1.52 +          val U = TVar (("'" ^ a, 0), [])
    1.53            val Ts = binder_types T;
    1.54            val i = length Ts;
    1.55            val xs = map (pair "x") Ts;
    1.56 @@ -98,8 +96,9 @@
    1.57  
    1.58  fun mk_realizes_eqn n vs nparms intrs =
    1.59    let
    1.60 -    val concl = HOLogic.dest_Trueprop (concl_of (hd intrs));
    1.61 -    val iTs = OldTerm.term_tvars concl;
    1.62 +    val intr = map_types Type.strip_sorts (prop_of (hd intrs));
    1.63 +    val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl intr);
    1.64 +    val iTs = rev (Term.add_tvars intr []);
    1.65      val Tvs = map TVar iTs;
    1.66      val (h as Const (s, T), us) = strip_comb concl;
    1.67      val params = List.take (us, nparms);
    1.68 @@ -110,7 +109,7 @@
    1.69        (Name.variant_list used (replicate (length elTs) "x") ~~ elTs);
    1.70      val rT = if n then Extraction.nullT
    1.71        else Type (space_implode "_" (s ^ "T" :: vs),
    1.72 -        map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs);
    1.73 +        map (fn a => TVar (("'" ^ a, 0), [])) vs @ Tvs);
    1.74      val r = if n then Extraction.nullt else Var ((Long_Name.base_name s, 0), rT);
    1.75      val S = list_comb (h, params @ xs);
    1.76      val rvs = relevant_vars S;
    1.77 @@ -121,7 +120,7 @@
    1.78        let val T = (the o AList.lookup (op =) rvs) v
    1.79        in (Const ("typeof", T --> Type ("Type", [])) $ Var ((v, 0), T),
    1.80          Extraction.mk_typ (if n then Extraction.nullT
    1.81 -          else TVar (("'" ^ v, 0), HOLogic.typeS)))
    1.82 +          else TVar (("'" ^ v, 0), [])))
    1.83        end;
    1.84  
    1.85      val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs;
    1.86 @@ -261,12 +260,12 @@
    1.87      val rlzvs = rev (Term.add_vars (prop_of rrule) []);
    1.88      val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
    1.89      val rs = map Var (subtract (op = o pairself fst) xs rlzvs);
    1.90 -    val rlz' = fold_rev Logic.all (vs2 @ rs) (prop_of rrule);
    1.91 -    val rlz'' = fold_rev Logic.all vs2 rlz
    1.92 +    val rlz' = fold_rev Logic.all rs (prop_of rrule)
    1.93    in (name, (vs,
    1.94      if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
    1.95 -    ProofRewriteRules.un_hhf_proof rlz' rlz''
    1.96 -      (fold_rev forall_intr_prf (vs2 @ rs) (prf_of rrule))))
    1.97 +    Extraction.abs_corr_shyps thy rule vs vs2
    1.98 +      (ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz)
    1.99 +         (fold_rev Proofterm.forall_intr_proof' rs (prf_of rrule)))))
   1.100    end;
   1.101  
   1.102  fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
   1.103 @@ -275,7 +274,7 @@
   1.104    let
   1.105      val qualifier = Long_Name.qualifier (name_of_thm induct);
   1.106      val inducts = PureThy.get_thms thy (Long_Name.qualify qualifier "inducts");
   1.107 -    val iTs = OldTerm.term_tvars (prop_of (hd intrs));
   1.108 +    val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []);
   1.109      val ar = length vs + length iTs;
   1.110      val params = Inductive.params_of raw_induct;
   1.111      val arities = Inductive.arities_of raw_induct;
   1.112 @@ -297,8 +296,6 @@
   1.113      val thy1' = thy1 |>
   1.114        Theory.copy |>
   1.115        Sign.add_types (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |>
   1.116 -      fold (fn s => AxClass.axiomatize_arity
   1.117 -        (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
   1.118          Extraction.add_typeof_eqns_i ty_eqs;
   1.119      val dts = map_filter (fn (s, rs) => if member (op =) rsets s then
   1.120        SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss;
   1.121 @@ -328,10 +325,10 @@
   1.122          end
   1.123        else (replicate (length rs) Extraction.nullt, (recs, dummies)))
   1.124          rss (rec_thms, dummies);
   1.125 -    val rintrs = map (fn (intr, c) => Envir.eta_contract
   1.126 +    val rintrs = map (fn (intr, c) => attach_typeS (Envir.eta_contract
   1.127        (Extraction.realizes_of thy2 vs
   1.128          (if c = Extraction.nullt then c else list_comb (c, map Var (rev
   1.129 -          (subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr)))
   1.130 +          (subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr))))
   1.131              (maps snd rss ~~ flat constrss);
   1.132      val (rlzpreds, rlzpreds') =
   1.133        rintrs |> map (fn rintr =>
   1.134 @@ -390,7 +387,9 @@
   1.135          val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
   1.136            (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
   1.137          val rews = map mk_meta_eq (@{thm fst_conv} :: @{thm snd_conv} :: rec_thms);
   1.138 -        val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY
   1.139 +        val thm = Goal.prove_global thy []
   1.140 +          (map attach_typeS prems) (attach_typeS concl)
   1.141 +          (fn {prems, ...} => EVERY
   1.142            [rtac (#raw_induct ind_info) 1,
   1.143             rewrite_goals_tac rews,
   1.144             REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
   1.145 @@ -408,10 +407,10 @@
   1.146        in
   1.147          Extraction.add_realizers_i
   1.148            (map (fn (((ind, corr), rlz), r) =>
   1.149 -              mk_realizer thy' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
   1.150 +              mk_realizer thy'' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
   1.151              realizers @ (case realizers of
   1.152               [(((ind, corr), rlz), r)] =>
   1.153 -               [mk_realizer thy' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
   1.154 +               [mk_realizer thy'' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
   1.155                    ind, corr, rlz, r)]
   1.156             | _ => [])) thy''
   1.157        end;
   1.158 @@ -445,7 +444,7 @@
   1.159              map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
   1.160              [Bound (length prems)]));
   1.161          val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim);
   1.162 -        val rlz' = strip_all (Logic.unvarify_global rlz);
   1.163 +        val rlz' = attach_typeS (strip_all (Logic.unvarify_global rlz));
   1.164          val rews = map mk_meta_eq case_thms;
   1.165          val thm = Goal.prove_global thy []
   1.166            (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn {prems, ...} => EVERY
   1.167 @@ -488,7 +487,7 @@
   1.168      val vss = sort (int_ord o pairself length)
   1.169        (subsets (map fst (relevant_vars (concl_of (hd intrs)))))
   1.170    in
   1.171 -    fold (add_ind_realizer rsets intrs induct raw_induct elims) vss thy
   1.172 +    fold_rev (add_ind_realizer rsets intrs induct raw_induct elims) vss thy
   1.173    end
   1.174  
   1.175  fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.mapping