src/HOL/Tools/record.ML
changeset 34151 8d57ce46b3f7
parent 33957 e9afca2118d4
child 35021 c839a4c670c6
     1.1 --- a/src/HOL/Tools/record.ML	Mon Dec 21 08:32:03 2009 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Mon Dec 21 08:32:04 2009 +0100
     1.3 @@ -50,24 +50,24 @@
     1.4  end;
     1.5  
     1.6  
     1.7 -signature ISTUPLE_SUPPORT =
     1.8 +signature ISO_TUPLE_SUPPORT =
     1.9  sig
    1.10 -  val add_istuple_type: bstring * string list -> typ * typ -> theory -> (term * term) * theory
    1.11 +  val add_iso_tuple_type: bstring * string list -> typ * typ -> theory -> (term * term) * theory
    1.12    val mk_cons_tuple: term * term -> term
    1.13    val dest_cons_tuple: term -> term * term
    1.14 -  val istuple_intros_tac: int -> tactic
    1.15 +  val iso_tuple_intros_tac: int -> tactic
    1.16    val named_cterm_instantiate: (string * cterm) list -> thm -> thm
    1.17  end;
    1.18  
    1.19 -structure IsTupleSupport: ISTUPLE_SUPPORT =
    1.20 +structure Iso_Tuple_Support: ISO_TUPLE_SUPPORT =
    1.21  struct
    1.22  
    1.23 -val isomN = "_TupleIsom";
    1.24 -
    1.25 -val istuple_intro = @{thm isomorphic_tuple_intro};
    1.26 -val istuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros};
    1.27 -
    1.28 -val tuple_istuple = (@{const_name tuple_istuple}, @{thm tuple_istuple});
    1.29 +val isoN = "_Tuple_Iso";
    1.30 +
    1.31 +val iso_tuple_intro = @{thm isomorphic_tuple_intro};
    1.32 +val iso_tuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros};
    1.33 +
    1.34 +val tuple_iso_tuple = (@{const_name tuple_iso_tuple}, @{thm tuple_iso_tuple});
    1.35  
    1.36  fun named_cterm_instantiate values thm =
    1.37    let
    1.38 @@ -81,10 +81,10 @@
    1.39      cterm_instantiate (map (apfst getvar) values) thm
    1.40    end;
    1.41  
    1.42 -structure IsTupleThms = Theory_Data
    1.43 +structure Iso_Tuple_Thms = Theory_Data
    1.44  (
    1.45    type T = thm Symtab.table;
    1.46 -  val empty = Symtab.make [tuple_istuple];
    1.47 +  val empty = Symtab.make [tuple_iso_tuple];
    1.48    val extend = I;
    1.49    fun merge data = Symtab.merge Thm.eq_thm_prop data;   (* FIXME handle Symtab.DUP ?? *)
    1.50  );
    1.51 @@ -96,7 +96,7 @@
    1.52          val SOME {Rep_inject = rep_inject, Abs_name = absN, abs_type = absT,
    1.53            Abs_inverse = abs_inverse, ...} = Typedef.get_info thy name;
    1.54          val rewrite_rule =
    1.55 -          MetaSimplifier.rewrite_rule [@{thm istuple_UNIV_I}, @{thm istuple_True_simp}];
    1.56 +          MetaSimplifier.rewrite_rule [@{thm iso_tuple_UNIV_I}, @{thm iso_tuple_True_simp}];
    1.57        in
    1.58          (map rewrite_rule [rep_inject, abs_inverse], Const (absN, repT --> absT), absT)
    1.59        end;
    1.60 @@ -112,14 +112,14 @@
    1.61      val prodT = HOLogic.mk_prodT (leftT, rightT);
    1.62      val isomT = Type (@{type_name tuple_isomorphism}, [prodT, leftT, rightT]);
    1.63    in
    1.64 -    Const (@{const_name istuple_cons}, isomT --> leftT --> rightT --> prodT) $
    1.65 -      Const (fst tuple_istuple, isomT) $ left $ right
    1.66 +    Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> prodT) $
    1.67 +      Const (fst tuple_iso_tuple, isomT) $ left $ right
    1.68    end;
    1.69  
    1.70 -fun dest_cons_tuple (Const (@{const_name istuple_cons}, _) $ Const _ $ t $ u) = (t, u)
    1.71 +fun dest_cons_tuple (Const (@{const_name iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u)
    1.72    | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);
    1.73  
    1.74 -fun add_istuple_type (name, alphas) (leftT, rightT) thy =
    1.75 +fun add_iso_tuple_type (name, alphas) (leftT, rightT) thy =
    1.76    let
    1.77      val repT = HOLogic.mk_prodT (leftT, rightT);
    1.78  
    1.79 @@ -131,39 +131,39 @@
    1.80      (*construct a type and body for the isomorphism constant by
    1.81        instantiating the theorem to which the definition will be applied*)
    1.82      val intro_inst =
    1.83 -      rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] istuple_intro;
    1.84 +      rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] iso_tuple_intro;
    1.85      val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst));
    1.86      val isomT = fastype_of body;
    1.87 -    val isom_bind = Binding.name (name ^ isomN);
    1.88 +    val isom_bind = Binding.name (name ^ isoN);
    1.89      val isom_name = Sign.full_name typ_thy isom_bind;
    1.90      val isom = Const (isom_name, isomT);
    1.91 -    val isom_spec = (Thm.def_name (name ^ isomN), Logic.mk_equals (isom, body));
    1.92 +    val isom_spec = (Thm.def_name (name ^ isoN), Logic.mk_equals (isom, body));
    1.93  
    1.94      val ([isom_def], cdef_thy) =
    1.95        typ_thy
    1.96        |> Sign.add_consts_i [Syntax.no_syn (isom_bind, isomT)]
    1.97        |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)];
    1.98  
    1.99 -    val istuple = isom_def RS (abs_inverse RS (rep_inject RS istuple_intro));
   1.100 -    val cons = Const (@{const_name istuple_cons}, isomT --> leftT --> rightT --> absT);
   1.101 +    val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
   1.102 +    val cons = Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> absT);
   1.103  
   1.104      val thm_thy =
   1.105        cdef_thy
   1.106 -      |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop (isom_name, istuple))
   1.107 +      |> Iso_Tuple_Thms.map (Symtab.insert Thm.eq_thm_prop (isom_name, iso_tuple))
   1.108        |> Sign.parent_path
   1.109        |> Code.add_default_eqn isom_def;
   1.110    in
   1.111      ((isom, cons $ isom), thm_thy)
   1.112    end;
   1.113  
   1.114 -val istuple_intros_tac = resolve_from_net_tac istuple_intros THEN'
   1.115 +val iso_tuple_intros_tac = resolve_from_net_tac iso_tuple_intros THEN'
   1.116    CSUBGOAL (fn (cgoal, i) =>
   1.117      let
   1.118        val thy = Thm.theory_of_cterm cgoal;
   1.119        val goal = Thm.term_of cgoal;
   1.120  
   1.121 -      val isthms = IsTupleThms.get thy;
   1.122 -      fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]);
   1.123 +      val isthms = Iso_Tuple_Thms.get thy;
   1.124 +      fun err s t = raise TERM ("iso_tuple_intros_tac: " ^ s, [t]);
   1.125  
   1.126        val goal' = Envir.beta_eta_contract goal;
   1.127        val is =
   1.128 @@ -197,13 +197,13 @@
   1.129  
   1.130  val refl_conj_eq = @{thm refl_conj_eq};
   1.131  
   1.132 -val surject_assistI = @{thm "istuple_surjective_proof_assistI"};
   1.133 -val surject_assist_idE = @{thm "istuple_surjective_proof_assist_idE"};
   1.134 +val surject_assistI = @{thm "iso_tuple_surjective_proof_assistI"};
   1.135 +val surject_assist_idE = @{thm "iso_tuple_surjective_proof_assist_idE"};
   1.136  
   1.137  val updacc_accessor_eqE = @{thm "update_accessor_accessor_eqE"};
   1.138  val updacc_updator_eqE = @{thm "update_accessor_updator_eqE"};
   1.139 -val updacc_eq_idI = @{thm "istuple_update_accessor_eq_assist_idI"};
   1.140 -val updacc_eq_triv = @{thm "istuple_update_accessor_eq_assist_triv"};
   1.141 +val updacc_eq_idI = @{thm "iso_tuple_update_accessor_eq_assist_idI"};
   1.142 +val updacc_eq_triv = @{thm "iso_tuple_update_accessor_eq_assist_triv"};
   1.143  
   1.144  val updacc_foldE = @{thm "update_accessor_congruence_foldE"};
   1.145  val updacc_unfoldE = @{thm "update_accessor_congruence_unfoldE"};
   1.146 @@ -211,7 +211,7 @@
   1.147  val updacc_noop_compE = @{thm "update_accessor_noop_compE"};
   1.148  val updacc_cong_idI = @{thm "update_accessor_cong_assist_idI"};
   1.149  val updacc_cong_triv = @{thm "update_accessor_cong_assist_triv"};
   1.150 -val updacc_cong_from_eq = @{thm "istuple_update_accessor_cong_from_eq"};
   1.151 +val updacc_cong_from_eq = @{thm "iso_tuple_update_accessor_cong_from_eq"};
   1.152  
   1.153  val o_eq_dest = @{thm o_eq_dest};
   1.154  val o_eq_id_dest = @{thm o_eq_id_dest};
   1.155 @@ -1066,7 +1066,7 @@
   1.156            Goal.prove (ProofContext.init thy) [] [] prop
   1.157              (fn _ =>
   1.158                simp_tac defset 1 THEN
   1.159 -              REPEAT_DETERM (IsTupleSupport.istuple_intros_tac 1) THEN
   1.160 +              REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
   1.161                TRY (simp_tac (HOL_ss addsimps id_o_apps) 1));
   1.162          val dest =
   1.163            if is_sel_upd_pair thy acc upd
   1.164 @@ -1089,7 +1089,7 @@
   1.165        Goal.prove (ProofContext.init thy) [] [] prop
   1.166          (fn _ =>
   1.167            simp_tac defset 1 THEN
   1.168 -          REPEAT_DETERM (IsTupleSupport.istuple_intros_tac 1) THEN
   1.169 +          REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
   1.170            TRY (simp_tac (HOL_ss addsimps [id_apply]) 1));
   1.171      val dest = if comp then o_eq_dest_lhs else o_eq_dest;
   1.172    in Drule.standard (othm RS dest) end;
   1.173 @@ -1117,7 +1117,7 @@
   1.174            else swaps_needed us (u :: prev) (Symtab.insert (K true) (cname u, ()) seen) swaps;
   1.175    in swaps_needed upd_funs [] Symtab.empty Symreltab.empty end;
   1.176  
   1.177 -val named_cterm_instantiate = IsTupleSupport.named_cterm_instantiate;
   1.178 +val named_cterm_instantiate = Iso_Tuple_Support.named_cterm_instantiate;
   1.179  
   1.180  fun prove_unfold_defs thy ex_simps ex_simprs prop =
   1.181    let
   1.182 @@ -1222,7 +1222,7 @@
   1.183      Goal.prove (ProofContext.init thy) [] [] prop
   1.184        (fn _ =>
   1.185          simp_tac simpset 1 THEN
   1.186 -        REPEAT_DETERM (IsTupleSupport.istuple_intros_tac 1) THEN
   1.187 +        REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
   1.188          TRY (resolve_tac [updacc_cong_idI] 1))
   1.189    end;
   1.190  
   1.191 @@ -1612,22 +1612,22 @@
   1.192      (*before doing anything else, create the tree of new types
   1.193        that will back the record extension*)
   1.194  
   1.195 -    val mktreeV = Balanced_Tree.make IsTupleSupport.mk_cons_tuple;
   1.196 -
   1.197 -    fun mk_istuple (left, right) (thy, i) =
   1.198 +    val mktreeV = Balanced_Tree.make Iso_Tuple_Support.mk_cons_tuple;
   1.199 +
   1.200 +    fun mk_iso_tuple (left, right) (thy, i) =
   1.201        let
   1.202          val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
   1.203          val nm = suffix suff (Long_Name.base_name name);
   1.204          val ((_, cons), thy') =
   1.205 -          IsTupleSupport.add_istuple_type
   1.206 +          Iso_Tuple_Support.add_iso_tuple_type
   1.207              (nm, alphas_zeta) (fastype_of left, fastype_of right) thy;
   1.208        in
   1.209          (cons $ left $ right, (thy', i + 1))
   1.210        end;
   1.211  
   1.212 -    (*trying to create a 1-element istuple will fail, and is pointless anyway*)
   1.213 -    fun mk_even_istuple [arg] = pair arg
   1.214 -      | mk_even_istuple args = mk_istuple (IsTupleSupport.dest_cons_tuple (mktreeV args));
   1.215 +    (*trying to create a 1-element iso_tuple will fail, and is pointless anyway*)
   1.216 +    fun mk_even_iso_tuple [arg] = pair arg
   1.217 +      | mk_even_iso_tuple args = mk_iso_tuple (Iso_Tuple_Support.dest_cons_tuple (mktreeV args));
   1.218  
   1.219      fun build_meta_tree_type i thy vars more =
   1.220        let val len = length vars in
   1.221 @@ -1637,12 +1637,12 @@
   1.222              fun group16 [] = []
   1.223                | group16 xs = take 16 xs :: group16 (drop 16 xs);
   1.224              val vars' = group16 vars;
   1.225 -            val (composites, (thy', i')) = fold_map mk_even_istuple vars' (thy, i);
   1.226 +            val (composites, (thy', i')) = fold_map mk_even_iso_tuple vars' (thy, i);
   1.227            in
   1.228              build_meta_tree_type i' thy' composites more
   1.229            end
   1.230          else
   1.231 -          let val (term, (thy', _)) = mk_istuple (mktreeV vars, more) (thy, 0)
   1.232 +          let val (term, (thy', _)) = mk_iso_tuple (mktreeV vars, more) (thy, 0)
   1.233            in (term, thy') end
   1.234        end;
   1.235  
   1.236 @@ -1712,7 +1712,7 @@
   1.237              simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
   1.238              REPEAT_DETERM
   1.239                (rtac refl_conj_eq 1 ORELSE
   1.240 -                IsTupleSupport.istuple_intros_tac 1 ORELSE
   1.241 +                Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
   1.242                  rtac refl 1)));
   1.243  
   1.244      val inject = timeit_msg "record extension inject proof:" inject_prf;
   1.245 @@ -1730,7 +1730,7 @@
   1.246          val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE;
   1.247          val tactic1 =
   1.248            simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
   1.249 -          REPEAT_ALL_NEW IsTupleSupport.istuple_intros_tac 1;
   1.250 +          REPEAT_ALL_NEW Iso_Tuple_Support.iso_tuple_intros_tac 1;
   1.251          val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
   1.252          val [halfway] = Seq.list_of (tactic1 start);
   1.253          val [surject] = Seq.list_of (tactic2 (Drule.standard halfway));
   1.254 @@ -1954,7 +1954,7 @@
   1.255  
   1.256      val ext_defs = ext_def :: map #extdef parents;
   1.257  
   1.258 -    (*Theorems from the istuple intros.
   1.259 +    (*Theorems from the iso_tuple intros.
   1.260        This is complex enough to deserve a full comment.
   1.261        By unfolding ext_defs from r_rec0 we create a tree of constructor
   1.262        calls (many of them Pair, but others as well). The introduction
   1.263 @@ -1979,7 +1979,7 @@
   1.264          val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
   1.265          val tactic =
   1.266            simp_tac (HOL_basic_ss addsimps ext_defs) 1 THEN
   1.267 -          REPEAT (IsTupleSupport.istuple_intros_tac 1 ORELSE terminal);
   1.268 +          REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE terminal);
   1.269          val updaccs = Seq.list_of (tactic init_thm);
   1.270        in
   1.271          (updaccs RL [updacc_accessor_eqE],
   1.272 @@ -2207,7 +2207,7 @@
   1.273               [rtac surject_assist_idE 1,
   1.274                simp_tac init_ss 1,
   1.275                REPEAT
   1.276 -                (IsTupleSupport.istuple_intros_tac 1 ORELSE
   1.277 +                (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
   1.278                    (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))])
   1.279        end;
   1.280      val surjective = timeit_msg "record surjective proof:" surjective_prf;