src/HOL/Tools/datatype_package.ML
changeset 7049 f59d33c6e1c7
parent 7015 85be09eb136c
child 7060 80d244f81b96
equal deleted inserted replaced
7048:3535eec33c50 7049:f59d33c6e1c7
   202   end;
   202   end;
   203 
   203 
   204 
   204 
   205 (**** simplification procedure for showing distinctness of constructors ****)
   205 (**** simplification procedure for showing distinctness of constructors ****)
   206 
   206 
   207 (* oracle *)
       
   208 
       
   209 val distinctN = "constr_distinct";
   207 val distinctN = "constr_distinct";
   210 
   208 
   211 exception ConstrDistinct of term;
   209 exception ConstrDistinct of term;
   212 
   210 
   213 
   211 
   246           | _ => None)
   244           | _ => None)
   247    | _ => None)
   245    | _ => None)
   248   | distinct_proc sg _ _ = None;
   246   | distinct_proc sg _ _ = None;
   249 
   247 
   250 val distinct_pats = [Thm.read_cterm (Theory.sign_of HOL.thy) ("s = t", HOLogic.termTVar)];
   248 val distinct_pats = [Thm.read_cterm (Theory.sign_of HOL.thy) ("s = t", HOLogic.termTVar)];
   251 val distinct_simproc = mk_simproc "distinct_simproc" distinct_pats distinct_proc;
   249 val distinct_simproc = mk_simproc distinctN distinct_pats distinct_proc;
   252 
   250 
   253 val dist_ss = HOL_ss addsimprocs [distinct_simproc];
   251 val dist_ss = HOL_ss addsimprocs [distinct_simproc];
   254 
   252 
   255 val simproc_setup =
   253 val simproc_setup =
   256   [Theory.add_oracle (distinctN, fn (_, ConstrDistinct t) => t),
   254   [Theory.add_oracle (distinctN, fn (_, ConstrDistinct t) => t),
   295        nchotomy = nchotomy,
   293        nchotomy = nchotomy,
   296        case_cong = case_cong});
   294        case_cong = case_cong});
   297 
   295 
   298 fun store_clasimp thy (cla, simp) =
   296 fun store_clasimp thy (cla, simp) =
   299   (claset_ref_of thy := cla; simpset_ref_of thy := simp);
   297   (claset_ref_of thy := cla; simpset_ref_of thy := simp);
   300 
       
   301 infix 4 addDistinct;
       
   302 
       
   303 fun clasimp addDistinct ([], _) = clasimp
       
   304   | clasimp addDistinct (thms::thmss, (_, (_, _, constrs))::descr) =
       
   305       if length constrs < !DatatypeProp.dtK then
       
   306         clasimp addIffs thms addDistinct (thmss, descr)
       
   307       else
       
   308         clasimp addsimps2 thms addDistinct (thmss, descr);
       
   309 
   298 
   310 
   299 
   311 (********************* axiomatic introduction of datatypes ********************)
   300 (********************* axiomatic introduction of datatypes ********************)
   312 
   301 
   313 fun add_and_get_axioms label tnames ts thy =
   302 fun add_and_get_axioms label tnames ts thy =