src/HOL/Tools/record.ML
changeset 32752 f65d74a264dd
parent 32749 3282c12a856c
child 32757 4e97fc468a53
     1.1 --- a/src/HOL/Tools/record.ML	Tue Sep 22 13:52:19 2009 +1000
     1.2 +++ b/src/HOL/Tools/record.ML	Wed Sep 23 19:17:48 2009 +1000
     1.3 @@ -52,6 +52,146 @@
     1.4  end;
     1.5  
     1.6  
     1.7 +signature ISTUPLE_SUPPORT =
     1.8 +sig
     1.9 +  val add_istuple_type: bstring * string list -> (typ * typ) -> theory ->
    1.10 +            (term * term * theory);
    1.11 +
    1.12 +  val mk_cons_tuple: term * term -> term;
    1.13 +  val dest_cons_tuple: term -> term * term;
    1.14 +
    1.15 +  val istuple_intros_tac: theory -> int -> tactic;
    1.16 +
    1.17 +  val named_cterm_instantiate: (string * cterm) list -> thm -> thm;
    1.18 +end;
    1.19 +
    1.20 +structure IsTupleSupport : ISTUPLE_SUPPORT =
    1.21 +struct
    1.22 +
    1.23 +val isomN = "_TupleIsom";
    1.24 +val defN = "_def";
    1.25 +
    1.26 +val istuple_UNIV_I = @{thm "istuple_UNIV_I"};
    1.27 +val istuple_True_simp = @{thm "istuple_True_simp"};
    1.28 +
    1.29 +val istuple_intro = @{thm "isomorphic_tuple_intro"};
    1.30 +val istuple_intros = build_net (@{thms "isomorphic_tuple.intros"});
    1.31 +
    1.32 +val constname = fst o dest_Const;
    1.33 +val tuple_istuple = (constname @{term tuple_istuple}, @{thm tuple_istuple});
    1.34 +
    1.35 +val istuple_constN = constname @{term isomorphic_tuple};
    1.36 +val istuple_consN = constname @{term istuple_cons};
    1.37 +
    1.38 +val tup_isom_typeN = fst (dest_Type @{typ "('a, 'b, 'c) tuple_isomorphism"});
    1.39 +
    1.40 +fun named_cterm_instantiate values thm = let
    1.41 +    fun match name (Var ((name', _), _)) = name = name'
    1.42 +      | match name _ = false;
    1.43 +    fun getvar name = case (find_first (match name)
    1.44 +                                    (OldTerm.term_vars (prop_of thm)))
    1.45 +      of SOME var => cterm_of (theory_of_thm thm) var
    1.46 +       | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm])
    1.47 +  in
    1.48 +    cterm_instantiate (map (apfst getvar) values) thm
    1.49 +  end;
    1.50 +
    1.51 +structure IsTupleThms = TheoryDataFun
    1.52 +(
    1.53 +  type T = thm Symtab.table;
    1.54 +  val empty = Symtab.make [tuple_istuple];
    1.55 +  val copy = I;
    1.56 +  val extend = I;
    1.57 +  val merge = K (Symtab.merge Thm.eq_thm_prop);
    1.58 +);
    1.59 +
    1.60 +fun do_typedef name repT alphas thy =
    1.61 +  let
    1.62 +    fun get_thms thy name =
    1.63 +      let
    1.64 +        val SOME { Rep_inject=rep_inject, Abs_name=absN, abs_type=absT,
    1.65 +          Abs_inverse=abs_inverse, ...} = Typedef.get_info thy name;
    1.66 +        val rewrite_rule = MetaSimplifier.rewrite_rule [istuple_UNIV_I, istuple_True_simp];
    1.67 +      in (map rewrite_rule [rep_inject, abs_inverse],
    1.68 +            Const (absN, repT --> absT), absT) end;
    1.69 +  in
    1.70 +    thy
    1.71 +    |> Typecopy.typecopy (Binding.name name, alphas) repT NONE
    1.72 +    |-> (fn (name, _) => `(fn thy => get_thms thy name))
    1.73 +  end;
    1.74 +
    1.75 +fun mk_cons_tuple (left, right) = let
    1.76 +    val (leftT, rightT) = (fastype_of left, fastype_of right);
    1.77 +    val prodT           = HOLogic.mk_prodT (leftT, rightT);
    1.78 +    val isomT           = Type (tup_isom_typeN, [prodT, leftT, rightT]);
    1.79 +  in
    1.80 +    Const (istuple_consN, isomT --> leftT --> rightT --> prodT)
    1.81 +      $ Const (fst tuple_istuple, isomT) $ left $ right
    1.82 +  end;
    1.83 +
    1.84 +fun dest_cons_tuple (v as Const (ic, _) $ Const _ $ left $ right)
    1.85 +  = if ic = istuple_consN then (left, right)
    1.86 +    else raise TERM ("dest_cons_tuple", [v])
    1.87 +  | dest_cons_tuple v = raise TERM ("dest_cons_tuple", [v]);
    1.88 +
    1.89 +fun add_istuple_type (name, alphas) (leftT, rightT) thy =
    1.90 +let
    1.91 +  val repT = HOLogic.mk_prodT (leftT, rightT);
    1.92 +
    1.93 +  val (([rep_inject, abs_inverse], absC, absT), typ_thy) =
    1.94 +    thy
    1.95 +    |> do_typedef name repT alphas
    1.96 +    ||> Sign.add_path name;
    1.97 +
    1.98 +  (* construct a type and body for the isomorphism constant by
    1.99 +     instantiating the theorem to which the definition will be applied *)
   1.100 +  val intro_inst = rep_inject RS
   1.101 +                   (named_cterm_instantiate [("abst", cterm_of typ_thy absC)]
   1.102 +                        istuple_intro);
   1.103 +  val (_, body)  = Logic.dest_equals (List.last (prems_of intro_inst));
   1.104 +  val isomT      = fastype_of body;
   1.105 +  val isom_bind  = Binding.name (name ^ isomN);
   1.106 +  val isom       = Const (Sign.full_name typ_thy isom_bind, isomT);
   1.107 +  val isom_spec  = (name ^ isomN ^ defN, Logic.mk_equals (isom, body));
   1.108 +
   1.109 +  val ([isom_def], cdef_thy) =
   1.110 +    typ_thy
   1.111 +    |> Sign.add_consts_i [Syntax.no_syn (isom_bind, isomT)]
   1.112 +    |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)];
   1.113 +
   1.114 +  val istuple = isom_def RS (abs_inverse RS (rep_inject RS istuple_intro));
   1.115 +  val cons    = Const (istuple_consN, isomT --> leftT --> rightT --> absT)
   1.116 +
   1.117 +  val thm_thy =
   1.118 +    cdef_thy
   1.119 +    |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop
   1.120 +                           (constname isom, istuple))
   1.121 +    |> Sign.parent_path;
   1.122 +in
   1.123 +  (isom, cons $ isom, thm_thy)
   1.124 +end;
   1.125 +
   1.126 +fun istuple_intros_tac thy = let
   1.127 +    val isthms  = IsTupleThms.get thy;
   1.128 +    fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]);
   1.129 +    val use_istuple_thm_tac = SUBGOAL (fn (goal, n) => let
   1.130 +        val goal' = Envir.beta_eta_contract goal;
   1.131 +        val isom  = case goal' of (Const tp $ (Const pr $ Const is))
   1.132 +                    => if fst tp = "Trueprop" andalso fst pr = istuple_constN
   1.133 +                       then Const is
   1.134 +                       else err "unexpected goal predicate" goal'
   1.135 +            | _ => err "unexpected goal format" goal';
   1.136 +        val isthm = case Symtab.lookup isthms (constname isom) of
   1.137 +                    SOME isthm => isthm
   1.138 +                  | NONE => err "no thm found for constant" isom;
   1.139 +      in rtac isthm n end);
   1.140 +  in
   1.141 +    fn n => resolve_from_net_tac istuple_intros n
   1.142 +            THEN use_istuple_thm_tac n
   1.143 +  end;
   1.144 +
   1.145 +end;
   1.146 +
   1.147  structure Record: RECORD =
   1.148  struct
   1.149  
   1.150 @@ -68,6 +208,7 @@
   1.151  val o_assoc = @{thm "o_assoc"};
   1.152  val id_apply = @{thm id_apply};
   1.153  val id_o_apps = [@{thm id_apply}, @{thm id_o}, @{thm o_id}];
   1.154 +val Not_eq_iff = @{thm Not_eq_iff};
   1.155  
   1.156  val refl_conj_eq = thm "refl_conj_eq";
   1.157  val meta_all_sameI = thm "meta_all_sameI";
   1.158 @@ -966,14 +1107,14 @@
   1.159      val T = range_type (fastype_of f);
   1.160    in mk_comp (Const ("Fun.id", T --> T)) f end;
   1.161  
   1.162 -fun get_updfuns (upd $ _ $ t) = upd :: get_updfuns t
   1.163 -  | get_updfuns _             = [];
   1.164 +fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t
   1.165 +  | get_upd_funs _             = [];
   1.166  
   1.167  fun get_accupd_simps thy term defset intros_tac = let
   1.168      val (acc, [body]) = strip_comb term;
   1.169      val recT          = domain_type (fastype_of acc);
   1.170 -    val updfuns       = sort_distinct TermOrd.fast_term_ord
   1.171 -                           (get_updfuns body);
   1.172 +    val upd_funs      = sort_distinct TermOrd.fast_term_ord
   1.173 +                           (get_upd_funs body);
   1.174      fun get_simp upd  = let
   1.175          val T    = domain_type (fastype_of upd);
   1.176          val lhs  = mk_comp acc (upd $ Free ("f", T));
   1.177 @@ -987,7 +1128,7 @@
   1.178          val dest = if is_sel_upd_pair thy acc upd
   1.179                     then o_eq_dest else o_eq_id_dest;
   1.180        in standard (othm RS dest) end;
   1.181 -  in map get_simp updfuns end;
   1.182 +  in map get_simp upd_funs end;
   1.183  
   1.184  structure SymSymTab = Table(type key = string * string
   1.185                              val ord = prod_ord fast_string_ord fast_string_ord);
   1.186 @@ -1009,26 +1150,26 @@
   1.187  
   1.188  fun get_updupd_simps thy term defset intros_tac = let
   1.189      val recT          = fastype_of term;
   1.190 -    val updfuns       = get_updfuns term;
   1.191 +    val upd_funs      = get_upd_funs term;
   1.192      val cname         = fst o dest_Const;
   1.193      fun getswap u u'  = get_updupd_simp thy defset intros_tac u u'
   1.194                                (cname u = cname u');
   1.195 -    fun buildswapstoeq upd [] swaps = swaps
   1.196 -      | buildswapstoeq upd (u::us) swaps = let
   1.197 +    fun build_swaps_to_eq upd [] swaps = swaps
   1.198 +      | build_swaps_to_eq upd (u::us) swaps = let
   1.199               val key      = (cname u, cname upd);
   1.200               val newswaps = if SymSymTab.defined swaps key then swaps
   1.201                              else SymSymTab.insert (K true)
   1.202                                       (key, getswap u upd) swaps;
   1.203            in if cname u = cname upd then newswaps
   1.204 -             else buildswapstoeq upd us newswaps end;
   1.205 -    fun swapsneeded []      prev seen swaps = map snd (SymSymTab.dest swaps)
   1.206 -      | swapsneeded (u::us) prev seen swaps =
   1.207 +             else build_swaps_to_eq upd us newswaps end;
   1.208 +    fun swaps_needed []      prev seen swaps = map snd (SymSymTab.dest swaps)
   1.209 +      | swaps_needed (u::us) prev seen swaps =
   1.210             if Symtab.defined seen (cname u)
   1.211 -           then swapsneeded us prev seen
   1.212 -                   (buildswapstoeq u prev swaps)
   1.213 -           else swapsneeded us (u::prev)
   1.214 +           then swaps_needed us prev seen
   1.215 +                   (build_swaps_to_eq u prev swaps)
   1.216 +           else swaps_needed us (u::prev)
   1.217                     (Symtab.insert (K true) (cname u, ()) seen) swaps;
   1.218 -  in swapsneeded updfuns [] Symtab.empty SymSymTab.empty end;
   1.219 +  in swaps_needed upd_funs [] Symtab.empty SymSymTab.empty end;
   1.220  
   1.221  val named_cterm_instantiate = IsTupleSupport.named_cterm_instantiate;
   1.222  
   1.223 @@ -2222,14 +2363,13 @@
   1.224  
   1.225      fun split_ex_prf () =
   1.226        let
   1.227 -        val ss   = HOL_basic_ss addsimps [not_ex RS sym, nth simp_thms 1];
   1.228 -        val [Pv] = OldTerm.term_vars (prop_of split_object);
   1.229 -        val cPv  = cterm_of defs_thy Pv;
   1.230 -        val cP   = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0)));
   1.231 -        val so3  = cterm_instantiate ([(cPv, cP)]) split_object;
   1.232 -        val so4  = simplify ss so3;
   1.233 +        val ss    = HOL_basic_ss addsimps [not_ex RS sym, Not_eq_iff];
   1.234 +        val P_nm  = fst (dest_Free P);
   1.235 +        val not_P = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0)));
   1.236 +        val so'   = named_cterm_instantiate ([(P_nm, not_P)]) split_object;
   1.237 +        val so''  = simplify ss so';
   1.238        in
   1.239 -        prove_standard [] split_ex_prop (fn prems => resolve_tac [so4] 1)
   1.240 +        prove_standard [] split_ex_prop (fn prems => resolve_tac [so''] 1)
   1.241        end;
   1.242      val split_ex = timeit_msg "record split_ex proof:" split_ex_prf;
   1.243