src/HOL/HOLCF/Tools/Domain/domain_induction.ML
changeset 41214 8a341cf54a85
parent 40832 4352ca878c41
child 41296 6aaf80ea9715
equal deleted inserted replaced
41194:9796e5e01b61 41214:8a341cf54a85
    56   end
    56   end
    57 
    57 
    58   fun prove_take_apps
    58   fun prove_take_apps
    59       ((dbind, take_const), constr_info) thy =
    59       ((dbind, take_const), constr_info) thy =
    60     let
    60     let
    61       val {iso_info, con_specs, con_betas, ...} = constr_info
    61       val {iso_info, con_specs, con_betas, ...} : Domain_Constructors.constr_info = constr_info
    62       val {abs_inverse, ...} = iso_info
    62       val {abs_inverse, ...} = iso_info
    63       fun prove_take_app (con_const, args) =
    63       fun prove_take_app (con_const, args) =
    64         let
    64         let
    65           val Ts = map snd args
    65           val Ts = map snd args
    66           val ns = Name.variant_list ["n"] (Datatype_Prop.make_tnames Ts)
    66           val ns = Name.variant_list ["n"] (Datatype_Prop.make_tnames Ts)
   218           if length dnames = 1 then ["adm"] else
   218           if length dnames = 1 then ["adm"] else
   219           map (fn s => "adm_" ^ Long_Name.base_name s) dnames
   219           map (fn s => "adm_" ^ Long_Name.base_name s) dnames
   220       val bottoms =
   220       val bottoms =
   221           if length dnames = 1 then ["bottom"] else
   221           if length dnames = 1 then ["bottom"] else
   222           map (fn s => "bottom_" ^ Long_Name.base_name s) dnames
   222           map (fn s => "bottom_" ^ Long_Name.base_name s) dnames
   223       fun one_eq bot constr_info =
   223       fun one_eq bot (constr_info : Domain_Constructors.constr_info) =
   224         let fun name_of (c, args) = Long_Name.base_name (fst (dest_Const c))
   224         let fun name_of (c, args) = Long_Name.base_name (fst (dest_Const c))
   225         in bot :: map name_of (#con_specs constr_info) end
   225         in bot :: map name_of (#con_specs constr_info) end
   226     in adms @ flat (map2 one_eq bottoms constr_infos) end
   226     in adms @ flat (map2 one_eq bottoms constr_infos) end
   227 
   227 
   228   val inducts = Project_Rule.projections (ProofContext.init_global thy) ind
   228   val inducts = Project_Rule.projections (ProofContext.init_global thy) ind