src/HOL/Tools/inductive_realizer.ML
changeset 13725 12404b452034
parent 13710 75bec2c1bfd5
child 13921 69c627b6b28d
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Mon Nov 25 20:32:29 2002 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Nov 27 17:06:47 2002 +0100
     1.3 @@ -69,22 +69,7 @@
     1.4      map constr_of_intr intrs)
     1.5    end;
     1.6  
     1.7 -fun gen_realizes (Const ("realizes", Type ("fun", [T, _])) $ t $
     1.8 -      (Const ("op :", Type ("fun", [U, _])) $ x $ Var (ixn, _))) =
     1.9 -        Var (ixn, [T, U] ---> HOLogic.boolT) $ t $ x
    1.10 -  | gen_realizes (Const ("op :", Type ("fun", [U, _])) $ x $ Var (ixn, _)) =
    1.11 -      Var (ixn, U --> HOLogic.boolT) $ x
    1.12 -  | gen_realizes (bla as Const ("realizes", Type ("fun", [T, _])) $ t $ P) =
    1.13 -      if T = Extraction.nullT then P
    1.14 -      else (case strip_comb P of
    1.15 -          (Var (ixn, U), ts) => list_comb (Var (ixn, T --> U), t :: ts)
    1.16 -        | _ => error "gen_realizes: variable expected")
    1.17 -  | gen_realizes (t $ u) = gen_realizes t $ gen_realizes u
    1.18 -  | gen_realizes (Abs (s, T, t)) = Abs (s, T, gen_realizes t)
    1.19 -  | gen_realizes t = t;
    1.20 -
    1.21  fun mk_rlz T = Const ("realizes", [T, HOLogic.boolT] ---> HOLogic.boolT);
    1.22 -fun mk_rlz' T = Const ("realizes", [T, propT] ---> propT);
    1.23  
    1.24  (** turn "P" into "%r x. realizes r (P x)" or "%r x. realizes r (x : P)" **)
    1.25  
    1.26 @@ -268,30 +253,26 @@
    1.27  
    1.28  fun mk_realizer thy vs params ((rule, rrule), rt) =
    1.29    let
    1.30 -    val prems = prems_of rule;
    1.31 +    val prems = prems_of rule ~~ prems_of rrule;
    1.32 +    val rvs = map fst (relevant_vars (prop_of rule));
    1.33      val xs = rev (Term.add_vars ([], prop_of rule));
    1.34 -    val rs = gen_rems (op = o pairself fst)
    1.35 -      (rev (Term.add_vars ([], prop_of rrule)), xs);
    1.36 +    val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs);
    1.37 +    val rlzvs = rev (Term.add_vars ([], prop_of rrule));
    1.38 +    val vs2 = map (fn (ixn, _) => Var (ixn, the (assoc (rlzvs, ixn)))) xs;
    1.39 +    val rs = gen_rems (op = o pairself fst) (rlzvs, xs);
    1.40  
    1.41      fun mk_prf _ [] prf = prf
    1.42 -      | mk_prf rs (prem :: prems) prf =
    1.43 -          let val T = Extraction.etype_of thy vs [] prem
    1.44 -          in if T = Extraction.nullT
    1.45 -            then AbsP ("H", Some (mk_rlz' T $ Extraction.nullt $ prem),
    1.46 -              mk_prf rs prems prf)
    1.47 -            else forall_intr_prf (Var (hd rs), AbsP ("H", Some (mk_rlz' T $
    1.48 -              Var (hd rs) $ prem), mk_prf (tl rs) prems prf))
    1.49 -          end;
    1.50 -
    1.51 -    val subst = map (fn v as (ixn, _) => (ixn, gen_rvar vs (Var v))) xs;
    1.52 -    val prf = Proofterm.map_proof_terms
    1.53 -      (subst_vars ([], subst)) I (prf_of rrule);
    1.54 +      | mk_prf rs ((prem, rprem) :: prems) prf =
    1.55 +          if Extraction.etype_of thy vs [] prem = Extraction.nullT
    1.56 +          then AbsP ("H", Some rprem, mk_prf rs prems prf)
    1.57 +          else forall_intr_prf (Var (hd rs), AbsP ("H", Some rprem,
    1.58 +            mk_prf (tl rs) prems prf));
    1.59  
    1.60    in (Thm.name_of_thm rule, (vs,
    1.61      if rt = Extraction.nullt then rt else
    1.62 -      foldr (uncurry lambda) (map Var xs, rt),
    1.63 -    foldr forall_intr_prf (map Var xs, mk_prf rs prems (Proofterm.proof_combP
    1.64 -      (prf, map PBound (length prems - 1 downto 0))))))
    1.65 +      foldr (uncurry lambda) (vs1, rt),
    1.66 +    foldr forall_intr_prf (vs2, mk_prf rs prems (Proofterm.proof_combP
    1.67 +      (prf_of rrule, map PBound (length prems - 1 downto 0))))))
    1.68    end;
    1.69  
    1.70  fun add_rule (rss, r) =
    1.71 @@ -348,10 +329,10 @@
    1.72          end
    1.73        else ((recs, dummies), replicate (length rs) Extraction.nullt))
    1.74          ((get #rec_thms dt_info, dummies), rss);
    1.75 -    val rintrs = map (fn (intr, c) => Pattern.eta_contract (gen_realizes
    1.76 +    val rintrs = map (fn (intr, c) => Pattern.eta_contract
    1.77        (Extraction.realizes_of thy2 vs
    1.78          c (prop_of (forall_intr_list (map (cterm_of (sign_of thy2) o Var)
    1.79 -          (rev (Term.add_vars ([], prop_of intr)) \\ params')) intr)))))
    1.80 +          (rev (Term.add_vars ([], prop_of intr)) \\ params')) intr))))
    1.81              (intrs ~~ flat constrss);
    1.82      val rlzsets = distinct (map (fn rintr => snd (HOLogic.dest_mem
    1.83        (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr)))) rintrs);
    1.84 @@ -377,8 +358,8 @@
    1.85        let
    1.86          val r = indrule_realizer thy induct raw_induct rsets params'
    1.87            (vs @ Ps) rec_names rss intrs dummies;
    1.88 -        val rlz = strip_all (Logic.unvarify (gen_realizes
    1.89 -          (Extraction.realizes_of thy (vs @ Ps) r (prop_of induct))));
    1.90 +        val rlz = strip_all (Logic.unvarify
    1.91 +          (Extraction.realizes_of thy (vs @ Ps) r (prop_of induct)));
    1.92          val rews = map mk_meta_eq
    1.93            (fst_conv :: snd_conv :: get #rec_thms dt_info);
    1.94          val thm = simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
    1.95 @@ -416,8 +397,8 @@
    1.96                 [Abs ("x", HOLogic.unitT, Const ("arbitrary", body_type T))]
    1.97               else []) @
    1.98              map Bound ((length prems - 1 downto 0) @ [length prems])));
    1.99 -        val rlz = strip_all (Logic.unvarify (gen_realizes
   1.100 -          (Extraction.realizes_of thy (vs @ Ps) r (prop_of elim))));
   1.101 +        val rlz = strip_all (Logic.unvarify
   1.102 +          (Extraction.realizes_of thy (vs @ Ps) r (prop_of elim)));
   1.103          val rews = map mk_meta_eq case_thms;
   1.104          val thm = simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
   1.105            [cut_facts_tac [hd prems] 1,