# HG changeset patch # User blanchet # Date 1367429629 -7200 # Node ID 106afdf5806c9e77d72fc5156a702bad1e553842 # Parent 19ee0cebe76d75a7175e32d6345bf5a457787b0a renamed a few FP-related files, to make it clear that these are not the sum of LFP + GFP but rather shared basic libraries diff -r 19ee0cebe76d -r 106afdf5806c src/HOL/BNF/BNF_FP.thy --- a/src/HOL/BNF/BNF_FP.thy Wed May 01 06:00:55 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,149 +0,0 @@ -(* Title: HOL/BNF/BNF_FP.thy - Author: Dmitriy Traytel, TU Muenchen - Author: Jasmin Blanchette, TU Muenchen - Copyright 2012 - -Basic fixed point operations on bounded natural functors. -*) - -header {* Basic Fixed Point Operations on Bounded Natural Functors *} - -theory BNF_FP -imports BNF_Comp BNF_Ctr_Sugar -keywords - "defaults" -begin - -lemma mp_conj: "(P \ Q) \ R \ P \ R \ Q" -by auto - -lemma eq_sym_Unity_conv: "(x = (() = ())) = x" -by blast - -lemma unit_case_Unity: "(case u of () => f) = f" -by (cases u) (hypsubst, rule unit.cases) - -lemma prod_case_Pair_iden: "(case p of (x, y) \ (x, y)) = p" -by simp - -lemma unit_all_impI: "(P () \ Q ()) \ \x. P x \ Q x" -by simp - -lemma prod_all_impI: "(\x y. P (x, y) \ Q (x, y)) \ \x. P x \ Q x" -by clarify - -lemma prod_all_impI_step: "(\x. \y. P (x, y) \ Q (x, y)) \ \x. P x \ Q x" -by auto - -lemma all_unit_eq: "(\x. PROP P x) \ PROP P ()" -by simp - -lemma all_prod_eq: "(\x. PROP P x) \ (\a b. PROP P (a, b))" -by clarsimp - -lemma rev_bspec: "a \ A \ \z \ A. P z \ P a" -by simp - -lemma Un_cong: "\A = B; C = D\ \ A \ C = B \ D" -by simp - -lemma pointfree_idE: "f \ g = id \ f (g x) = x" -unfolding o_def fun_eq_iff by simp - -lemma o_bij: - assumes gf: "g \ f = id" and fg: "f \ g = id" - shows "bij f" -unfolding bij_def inj_on_def surj_def proof safe - fix a1 a2 assume "f a1 = f a2" - hence "g ( f a1) = g (f a2)" by simp - thus "a1 = a2" using gf unfolding fun_eq_iff by simp -next - fix b - have "b = f (g b)" - using fg unfolding fun_eq_iff by simp - thus "EX a. b = f a" by blast -qed - -lemma ssubst_mem: "\t = s; s \ X\ \ t \ X" by simp - -lemma sum_case_step: -"sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p" -"sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p" -by auto - -lemma one_pointE: "\\x. s = x \ P\ \ P" -by simp - -lemma obj_one_pointE: "\x. s = x \ P \ P" -by blast - -lemma obj_sumE_f': -"\\x. s = f (Inl x) \ P; \x. s = f (Inr x) \ P\ \ s = f x \ P" -by (cases x) blast+ - -lemma obj_sumE_f: -"\\x. s = f (Inl x) \ P; \x. s = f (Inr x) \ P\ \ \x. s = f x \ P" -by (rule allI) (rule obj_sumE_f') - -lemma obj_sumE: "\\x. s = Inl x \ P; \x. s = Inr x \ P\ \ P" -by (cases s) auto - -lemma obj_sum_step': -"\\x. s = f (Inr (Inl x)) \ P; \x. s = f (Inr (Inr x)) \ P\ \ s = f (Inr x) \ P" -by (cases x) blast+ - -lemma obj_sum_step: -"\\x. s = f (Inr (Inl x)) \ P; \x. s = f (Inr (Inr x)) \ P\ \ \x. s = f (Inr x) \ P" -by (rule allI) (rule obj_sum_step') - -lemma sum_case_if: -"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)" -by simp - -lemma sum_case_o_inj: -"sum_case f g \ Inl = f" -"sum_case f g \ Inr = g" -by auto - -lemma ident_o_ident: "(\x. x) \ (\x. x) = (\x. x)" -by (rule o_def) - -lemma mem_UN_compreh_eq: "(z : \{y. \x\A. y = F x}) = (\x\A. z : F x)" -by blast - -lemma UN_compreh_eq_eq: -"\{y. \x\A. y = {}} = {}" -"\{y. \x\A. y = {x}} = A" -by blast+ - -lemma Inl_Inr_False: "(Inl x = Inr y) = False" -by simp - -lemma prod_set_simps: -"fsts (x, y) = {x}" -"snds (x, y) = {y}" -unfolding fsts_def snds_def by simp+ - -lemma sum_set_simps: -"setl (Inl x) = {x}" -"setl (Inr x) = {}" -"setr (Inl x) = {}" -"setr (Inr x) = {x}" -unfolding sum_set_defs by simp+ - -lemma prod_rel_simp: -"prod_rel P Q (x, y) (x', y') \ P x x' \ Q y y'" -unfolding prod_rel_def by simp - -lemma sum_rel_simps: -"sum_rel P Q (Inl x) (Inl x') \ P x x'" -"sum_rel P Q (Inr y) (Inr y') \ Q y y'" -"sum_rel P Q (Inl x) (Inr y') \ False" -"sum_rel P Q (Inr y) (Inl x') \ False" -unfolding sum_rel_def by simp+ - -ML_file "Tools/bnf_fp.ML" -ML_file "Tools/bnf_fp_def_sugar_tactics.ML" -ML_file "Tools/bnf_fp_def_sugar.ML" - -end diff -r 19ee0cebe76d -r 106afdf5806c src/HOL/BNF/BNF_FP_Basic.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BNF/BNF_FP_Basic.thy Wed May 01 19:33:49 2013 +0200 @@ -0,0 +1,149 @@ +(* Title: HOL/BNF/BNF_FP_Basic.thy + Author: Dmitriy Traytel, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012 + +Basic fixed point operations on bounded natural functors. +*) + +header {* Basic Fixed Point Operations on Bounded Natural Functors *} + +theory BNF_FP_Basic +imports BNF_Comp BNF_Ctr_Sugar +keywords + "defaults" +begin + +lemma mp_conj: "(P \ Q) \ R \ P \ R \ Q" +by auto + +lemma eq_sym_Unity_conv: "(x = (() = ())) = x" +by blast + +lemma unit_case_Unity: "(case u of () => f) = f" +by (cases u) (hypsubst, rule unit.cases) + +lemma prod_case_Pair_iden: "(case p of (x, y) \ (x, y)) = p" +by simp + +lemma unit_all_impI: "(P () \ Q ()) \ \x. P x \ Q x" +by simp + +lemma prod_all_impI: "(\x y. P (x, y) \ Q (x, y)) \ \x. P x \ Q x" +by clarify + +lemma prod_all_impI_step: "(\x. \y. P (x, y) \ Q (x, y)) \ \x. P x \ Q x" +by auto + +lemma all_unit_eq: "(\x. PROP P x) \ PROP P ()" +by simp + +lemma all_prod_eq: "(\x. PROP P x) \ (\a b. PROP P (a, b))" +by clarsimp + +lemma rev_bspec: "a \ A \ \z \ A. P z \ P a" +by simp + +lemma Un_cong: "\A = B; C = D\ \ A \ C = B \ D" +by simp + +lemma pointfree_idE: "f \ g = id \ f (g x) = x" +unfolding o_def fun_eq_iff by simp + +lemma o_bij: + assumes gf: "g \ f = id" and fg: "f \ g = id" + shows "bij f" +unfolding bij_def inj_on_def surj_def proof safe + fix a1 a2 assume "f a1 = f a2" + hence "g ( f a1) = g (f a2)" by simp + thus "a1 = a2" using gf unfolding fun_eq_iff by simp +next + fix b + have "b = f (g b)" + using fg unfolding fun_eq_iff by simp + thus "EX a. b = f a" by blast +qed + +lemma ssubst_mem: "\t = s; s \ X\ \ t \ X" by simp + +lemma sum_case_step: +"sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p" +"sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p" +by auto + +lemma one_pointE: "\\x. s = x \ P\ \ P" +by simp + +lemma obj_one_pointE: "\x. s = x \ P \ P" +by blast + +lemma obj_sumE_f': +"\\x. s = f (Inl x) \ P; \x. s = f (Inr x) \ P\ \ s = f x \ P" +by (cases x) blast+ + +lemma obj_sumE_f: +"\\x. s = f (Inl x) \ P; \x. s = f (Inr x) \ P\ \ \x. s = f x \ P" +by (rule allI) (rule obj_sumE_f') + +lemma obj_sumE: "\\x. s = Inl x \ P; \x. s = Inr x \ P\ \ P" +by (cases s) auto + +lemma obj_sum_step': +"\\x. s = f (Inr (Inl x)) \ P; \x. s = f (Inr (Inr x)) \ P\ \ s = f (Inr x) \ P" +by (cases x) blast+ + +lemma obj_sum_step: +"\\x. s = f (Inr (Inl x)) \ P; \x. s = f (Inr (Inr x)) \ P\ \ \x. s = f (Inr x) \ P" +by (rule allI) (rule obj_sum_step') + +lemma sum_case_if: +"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)" +by simp + +lemma sum_case_o_inj: +"sum_case f g \ Inl = f" +"sum_case f g \ Inr = g" +by auto + +lemma ident_o_ident: "(\x. x) \ (\x. x) = (\x. x)" +by (rule o_def) + +lemma mem_UN_compreh_eq: "(z : \{y. \x\A. y = F x}) = (\x\A. z : F x)" +by blast + +lemma UN_compreh_eq_eq: +"\{y. \x\A. y = {}} = {}" +"\{y. \x\A. y = {x}} = A" +by blast+ + +lemma Inl_Inr_False: "(Inl x = Inr y) = False" +by simp + +lemma prod_set_simps: +"fsts (x, y) = {x}" +"snds (x, y) = {y}" +unfolding fsts_def snds_def by simp+ + +lemma sum_set_simps: +"setl (Inl x) = {x}" +"setl (Inr x) = {}" +"setr (Inl x) = {}" +"setr (Inr x) = {x}" +unfolding sum_set_defs by simp+ + +lemma prod_rel_simp: +"prod_rel P Q (x, y) (x', y') \ P x x' \ Q y y'" +unfolding prod_rel_def by simp + +lemma sum_rel_simps: +"sum_rel P Q (Inl x) (Inl x') \ P x x'" +"sum_rel P Q (Inr y) (Inr y') \ Q y y'" +"sum_rel P Q (Inl x) (Inr y') \ False" +"sum_rel P Q (Inr y) (Inl x') \ False" +unfolding sum_rel_def by simp+ + +ML_file "Tools/bnf_fp_util.ML" +ML_file "Tools/bnf_fp_def_sugar_tactics.ML" +ML_file "Tools/bnf_fp_def_sugar.ML" + +end diff -r 19ee0cebe76d -r 106afdf5806c src/HOL/BNF/BNF_GFP.thy --- a/src/HOL/BNF/BNF_GFP.thy Wed May 01 06:00:55 2013 +0200 +++ b/src/HOL/BNF/BNF_GFP.thy Wed May 01 19:33:49 2013 +0200 @@ -8,7 +8,7 @@ header {* Greatest Fixed Point Operation on Bounded Natural Functors *} theory BNF_GFP -imports BNF_FP Equiv_Relations_More "~~/src/HOL/Library/Sublist" +imports BNF_FP_Basic Equiv_Relations_More "~~/src/HOL/Library/Sublist" keywords "codatatype" :: thy_decl begin diff -r 19ee0cebe76d -r 106afdf5806c src/HOL/BNF/BNF_LFP.thy --- a/src/HOL/BNF/BNF_LFP.thy Wed May 01 06:00:55 2013 +0200 +++ b/src/HOL/BNF/BNF_LFP.thy Wed May 01 19:33:49 2013 +0200 @@ -8,7 +8,7 @@ header {* Least Fixed Point Operation on Bounded Natural Functors *} theory BNF_LFP -imports BNF_FP +imports BNF_FP_Basic keywords "datatype_new" :: thy_decl begin diff -r 19ee0cebe76d -r 106afdf5806c src/HOL/BNF/Tools/bnf_fp.ML --- a/src/HOL/BNF/Tools/bnf_fp.ML Wed May 01 06:00:55 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,494 +0,0 @@ -(* Title: HOL/BNF/Tools/bnf_fp.ML - Author: Dmitriy Traytel, TU Muenchen - Author: Jasmin Blanchette, TU Muenchen - Copyright 2012, 2013 - -Shared library for the datatype and codatatype constructions. -*) - -signature BNF_FP = -sig - type fp_result = - {bnfs: BNF_Def.bnf list, - ctors: term list, - dtors: term list, - folds: term list, - recs: term list, - induct: thm, - strong_induct: thm, - dtor_ctors: thm list, - ctor_dtors: thm list, - ctor_injects: thm list, - map_thms: thm list, - set_thmss: thm list list, - rel_thms: thm list, - fold_thms: thm list, - rec_thms: thm list} - - val fp_name_of_ctor: term -> string - val morph_fp_result: morphism -> fp_result -> fp_result - val eq_fp_result: fp_result * fp_result -> bool - - val time: Timer.real_timer -> string -> Timer.real_timer - - val IITN: string - val LevN: string - val algN: string - val behN: string - val bisN: string - val carTN: string - val caseN: string - val coN: string - val coinductN: string - val corecN: string - val ctorN: string - val ctor_dtorN: string - val ctor_dtor_corecN: string - val ctor_dtor_unfoldN: string - val ctor_exhaustN: string - val ctor_induct2N: string - val ctor_inductN: string - val ctor_injectN: string - val ctor_foldN: string - val ctor_fold_uniqueN: string - val ctor_mapN: string - val ctor_map_uniqueN: string - val ctor_recN: string - val ctor_rec_uniqueN: string - val ctor_relN: string - val ctor_set_inclN: string - val ctor_set_set_inclN: string - val ctor_srelN: string - val disc_unfoldN: string - val disc_unfold_iffN: string - val disc_corecN: string - val disc_corec_iffN: string - val dtorN: string - val dtor_coinductN: string - val dtor_corecN: string - val dtor_corec_uniqueN: string - val dtor_ctorN: string - val dtor_exhaustN: string - val dtor_injectN: string - val dtor_mapN: string - val dtor_map_coinductN: string - val dtor_map_strong_coinductN: string - val dtor_map_uniqueN: string - val dtor_relN: string - val dtor_set_inclN: string - val dtor_set_set_inclN: string - val dtor_srelN: string - val dtor_srel_coinductN: string - val dtor_srel_strong_coinductN: string - val dtor_strong_coinductN: string - val dtor_unfoldN: string - val dtor_unfold_uniqueN: string - val exhaustN: string - val foldN: string - val hsetN: string - val hset_recN: string - val inductN: string - val injectN: string - val isNodeN: string - val lsbisN: string - val mapN: string - val map_uniqueN: string - val min_algN: string - val morN: string - val nchotomyN: string - val recN: string - val rel_injectN: string - val rel_distinctN: string - val rvN: string - val sel_corecN: string - val set_inclN: string - val set_set_inclN: string - val sel_unfoldN: string - val setsN: string - val simpsN: string - val strTN: string - val str_initN: string - val strong_coinductN: string - val sum_bdN: string - val sum_bdTN: string - val unfoldN: string - val uniqueN: string - - (* TODO: Don't index set facts. Isabelle packages traditionally generate uniform names. *) - val mk_ctor_setN: int -> string - val mk_dtor_setN: int -> string - val mk_dtor_set_inductN: int -> string - val mk_set_inductN: int -> string - - val mk_common_name: string list -> string - - val split_conj_thm: thm -> thm list - val split_conj_prems: int -> thm -> thm - - val mk_sumTN: typ list -> typ - val mk_sumTN_balanced: typ list -> typ - - val id_const: typ -> term - - val Inl_const: typ -> typ -> term - val Inr_const: typ -> typ -> term - - val mk_Inl: typ -> term -> term - val mk_Inr: typ -> term -> term - val mk_InN: typ list -> term -> int -> term - val mk_InN_balanced: typ -> int -> term -> int -> term - val mk_sum_case: term * term -> term - val mk_sum_caseN: term list -> term - val mk_sum_caseN_balanced: term list -> term - - val dest_sumT: typ -> typ * typ - val dest_sumTN: int -> typ -> typ list - val dest_sumTN_balanced: int -> typ -> typ list - val dest_tupleT: int -> typ -> typ list - - val mk_Field: term -> term - val mk_If: term -> term -> term -> term - val mk_union: term * term -> term - - val mk_sumEN: int -> thm - val mk_sumEN_balanced: int -> thm - val mk_sumEN_tupled_balanced: int list -> thm - val mk_sum_casesN: int -> int -> thm - val mk_sum_casesN_balanced: int -> int -> thm - - val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list - - val fp_bnf: (mixfix list -> (string * sort) list option -> binding list -> binding list -> - binding list -> binding list list -> typ list * typ list list -> BNF_Def.bnf list -> - local_theory -> 'a) -> - binding list -> mixfix list -> binding list -> binding list -> binding list list -> - (string * sort) list -> ((string * sort) * typ) list -> local_theory -> BNF_Def.bnf list * 'a -end; - -structure BNF_FP : BNF_FP = -struct - -open BNF_Comp -open BNF_Def -open BNF_Util - -type fp_result = - {bnfs: BNF_Def.bnf list, - ctors: term list, - dtors: term list, - folds: term list, - recs: term list, - induct: thm, - strong_induct: thm, - dtor_ctors: thm list, - ctor_dtors: thm list, - ctor_injects: thm list, - map_thms: thm list, - set_thmss: thm list list, - rel_thms: thm list, - fold_thms: thm list, - rec_thms: thm list}; - -val fp_name_of_ctor = fst o dest_Type o range_type o fastype_of; - -fun morph_fp_result phi {bnfs, ctors, dtors, folds, recs, induct, strong_induct, dtor_ctors, - ctor_dtors, ctor_injects, map_thms, set_thmss, rel_thms, fold_thms, rec_thms} = - {bnfs = map (morph_bnf phi) bnfs, - ctors = map (Morphism.term phi) ctors, - dtors = map (Morphism.term phi) dtors, - folds = map (Morphism.term phi) folds, - recs = map (Morphism.term phi) recs, - induct = Morphism.thm phi induct, - strong_induct = Morphism.thm phi strong_induct, - dtor_ctors = map (Morphism.thm phi) dtor_ctors, - ctor_dtors = map (Morphism.thm phi) ctor_dtors, - ctor_injects = map (Morphism.thm phi) ctor_injects, - map_thms = map (Morphism.thm phi) map_thms, - set_thmss = map (map (Morphism.thm phi)) set_thmss, - rel_thms = map (Morphism.thm phi) rel_thms, - fold_thms = map (Morphism.thm phi) fold_thms, - rec_thms = map (Morphism.thm phi) rec_thms}; - -fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) = - eq_list eq_bnf (bnfs1, bnfs2); - -val timing = true; -fun time timer msg = (if timing - then warning (msg ^ ": " ^ ATP_Util.string_from_time (Timer.checkRealTimer timer)) - else (); Timer.startRealTimer ()); - -val preN = "pre_" -val rawN = "raw_" - -val coN = "co" -val unN = "un" -val algN = "alg" -val IITN = "IITN" -val foldN = "fold" -val unfoldN = unN ^ foldN -val uniqueN = "_unique" -val simpsN = "simps" -val ctorN = "ctor" -val dtorN = "dtor" -val ctor_foldN = ctorN ^ "_" ^ foldN -val dtor_unfoldN = dtorN ^ "_" ^ unfoldN -val ctor_fold_uniqueN = ctor_foldN ^ uniqueN -val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN -val ctor_dtor_unfoldN = ctorN ^ "_" ^ dtor_unfoldN -val ctor_mapN = ctorN ^ "_" ^ mapN -val dtor_mapN = dtorN ^ "_" ^ mapN -val map_uniqueN = mapN ^ uniqueN -val ctor_map_uniqueN = ctorN ^ "_" ^ map_uniqueN -val dtor_map_uniqueN = dtorN ^ "_" ^ map_uniqueN -val min_algN = "min_alg" -val morN = "mor" -val bisN = "bis" -val lsbisN = "lsbis" -val sum_bdTN = "sbdT" -val sum_bdN = "sbd" -val carTN = "carT" -val strTN = "strT" -val isNodeN = "isNode" -val LevN = "Lev" -val rvN = "recover" -val behN = "beh" -val setsN = "sets" -val mk_ctor_setN = prefix (ctorN ^ "_") o mk_setN -val mk_dtor_setN = prefix (dtorN ^ "_") o mk_setN -fun mk_set_inductN i = mk_setN i ^ "_induct" -val mk_dtor_set_inductN = prefix (dtorN ^ "_") o mk_set_inductN - -val str_initN = "str_init" -val recN = "rec" -val corecN = coN ^ recN -val ctor_recN = ctorN ^ "_" ^ recN -val ctor_rec_uniqueN = ctor_recN ^ uniqueN -val dtor_corecN = dtorN ^ "_" ^ corecN -val dtor_corec_uniqueN = dtor_corecN ^ uniqueN -val ctor_dtor_corecN = ctorN ^ "_" ^ dtor_corecN - -val ctor_dtorN = ctorN ^ "_" ^ dtorN -val dtor_ctorN = dtorN ^ "_" ^ ctorN -val nchotomyN = "nchotomy" -val injectN = "inject" -val exhaustN = "exhaust" -val ctor_injectN = ctorN ^ "_" ^ injectN -val ctor_exhaustN = ctorN ^ "_" ^ exhaustN -val dtor_injectN = dtorN ^ "_" ^ injectN -val dtor_exhaustN = dtorN ^ "_" ^ exhaustN -val ctor_relN = ctorN ^ "_" ^ relN -val dtor_relN = dtorN ^ "_" ^ relN -val ctor_srelN = ctorN ^ "_" ^ srelN -val dtor_srelN = dtorN ^ "_" ^ srelN -val inductN = "induct" -val coinductN = coN ^ inductN -val ctor_inductN = ctorN ^ "_" ^ inductN -val ctor_induct2N = ctor_inductN ^ "2" -val dtor_map_coinductN = dtor_mapN ^ "_" ^ coinductN -val dtor_coinductN = dtorN ^ "_" ^ coinductN -val dtor_srel_coinductN = dtor_srelN ^ "_" ^ coinductN -val strong_coinductN = "strong_" ^ coinductN -val dtor_map_strong_coinductN = dtor_mapN ^ "_" ^ strong_coinductN -val dtor_strong_coinductN = dtorN ^ "_" ^ strong_coinductN -val dtor_srel_strong_coinductN = dtor_srelN ^ "_" ^ strong_coinductN -val hsetN = "Hset" -val hset_recN = hsetN ^ "_rec" -val set_inclN = "set_incl" -val ctor_set_inclN = ctorN ^ "_" ^ set_inclN -val dtor_set_inclN = dtorN ^ "_" ^ set_inclN -val set_set_inclN = "set_set_incl" -val ctor_set_set_inclN = ctorN ^ "_" ^ set_set_inclN -val dtor_set_set_inclN = dtorN ^ "_" ^ set_set_inclN - -val caseN = "case" -val discN = "disc" -val disc_unfoldN = discN ^ "_" ^ unfoldN -val disc_corecN = discN ^ "_" ^ corecN -val iffN = "_iff" -val disc_unfold_iffN = discN ^ "_" ^ unfoldN ^ iffN -val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN -val distinctN = "distinct" -val rel_distinctN = relN ^ "_" ^ distinctN -val injectN = "inject" -val rel_injectN = relN ^ "_" ^ injectN -val selN = "sel" -val sel_unfoldN = selN ^ "_" ^ unfoldN -val sel_corecN = selN ^ "_" ^ corecN - -val mk_common_name = space_implode "_"; - -fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T'); - -fun dest_sumTN 1 T = [T] - | dest_sumTN n (Type (@{type_name sum}, [T, T'])) = T :: dest_sumTN (n - 1) T'; - -val dest_sumTN_balanced = Balanced_Tree.dest dest_sumT; - -(* TODO: move something like this to "HOLogic"? *) -fun dest_tupleT 0 @{typ unit} = [] - | dest_tupleT 1 T = [T] - | dest_tupleT n (Type (@{type_name prod}, [T, T'])) = T :: dest_tupleT (n - 1) T'; - -val mk_sumTN = Library.foldr1 mk_sumT; -val mk_sumTN_balanced = Balanced_Tree.make mk_sumT; - -fun id_const T = Const (@{const_name id}, T --> T); - -fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT)); -fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t; - -fun Inr_const LT RT = Const (@{const_name Inr}, RT --> mk_sumT (LT, RT)); -fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t; - -fun mk_InN [_] t 1 = t - | mk_InN (_ :: Ts) t 1 = mk_Inl (mk_sumTN Ts) t - | mk_InN (LT :: Ts) t m = mk_Inr LT (mk_InN Ts t (m - 1)) - | mk_InN Ts t _ = raise (TYPE ("mk_InN", Ts, [t])); - -fun mk_InN_balanced sum_T n t k = - let - fun repair_types T (Const (s as @{const_name Inl}, _) $ t) = repair_inj_types T s fst t - | repair_types T (Const (s as @{const_name Inr}, _) $ t) = repair_inj_types T s snd t - | repair_types _ t = t - and repair_inj_types T s get t = - let val T' = get (dest_sumT T) in - Const (s, T' --> T) $ repair_types T' t - end; - in - Balanced_Tree.access {left = mk_Inl dummyT, right = mk_Inr dummyT, init = t} n k - |> repair_types sum_T - end; - -fun mk_sum_case (f, g) = - let - val fT = fastype_of f; - val gT = fastype_of g; - in - Const (@{const_name sum_case}, - fT --> gT --> mk_sumT (domain_type fT, domain_type gT) --> range_type fT) $ f $ g - end; - -val mk_sum_caseN = Library.foldr1 mk_sum_case; -val mk_sum_caseN_balanced = Balanced_Tree.make mk_sum_case; - -fun mk_If p t f = - let val T = fastype_of t; - in Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ p $ t $ f end; - -fun mk_Field r = - let val T = fst (dest_relT (fastype_of r)); - in Const (@{const_name Field}, mk_relT (T, T) --> HOLogic.mk_setT T) $ r end; - -val mk_union = HOLogic.mk_binop @{const_name sup}; - -(*dangerous; use with monotonic, converging functions only!*) -fun fixpoint eq f X = if subset eq (f X, X) then X else fixpoint eq f (f X); - -(* stolen from "~~/src/HOL/Tools/Datatype/datatype_aux.ML" *) -fun split_conj_thm th = - ((th RS conjunct1) :: split_conj_thm (th RS conjunct2)) handle THM _ => [th]; - -fun split_conj_prems limit th = - let - fun split n i th = - if i = n then th else split n (i + 1) (conjI RSN (i, th)) handle THM _ => th; - in split limit 1 th end; - -fun mk_sumEN 1 = @{thm one_pointE} - | mk_sumEN 2 = @{thm sumE} - | mk_sumEN n = - (fold (fn i => fn thm => @{thm obj_sum_step} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF - replicate n (impI RS allI); - -fun mk_obj_sumEN_balanced n = - Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f}))) - (replicate n asm_rl); - -fun mk_sumEN_balanced' n all_impIs = mk_obj_sumEN_balanced n OF all_impIs RS @{thm obj_one_pointE}; - -fun mk_sumEN_balanced 1 = @{thm one_pointE} (*optimization*) - | mk_sumEN_balanced 2 = @{thm sumE} (*optimization*) - | mk_sumEN_balanced n = mk_sumEN_balanced' n (replicate n (impI RS allI)); - -fun mk_tupled_allIN 0 = @{thm unit_all_impI} - | mk_tupled_allIN 1 = @{thm impI[THEN allI]} - | mk_tupled_allIN 2 = @{thm prod_all_impI} (*optimization*) - | mk_tupled_allIN n = mk_tupled_allIN (n - 1) RS @{thm prod_all_impI_step}; - -fun mk_sumEN_tupled_balanced ms = - let val n = length ms in - if forall (curry (op =) 1) ms then mk_sumEN_balanced n - else mk_sumEN_balanced' n (map mk_tupled_allIN ms) - end; - -fun mk_sum_casesN 1 1 = refl - | mk_sum_casesN _ 1 = @{thm sum.cases(1)} - | mk_sum_casesN 2 2 = @{thm sum.cases(2)} - | mk_sum_casesN n k = trans OF [@{thm sum_case_step(2)}, mk_sum_casesN (n - 1) (k - 1)]; - -fun mk_sum_step base step thm = - if Thm.eq_thm_prop (thm, refl) then base else trans OF [step, thm]; - -fun mk_sum_casesN_balanced 1 1 = refl - | mk_sum_casesN_balanced n k = - Balanced_Tree.access {left = mk_sum_step @{thm sum.cases(1)} @{thm sum_case_step(1)}, - right = mk_sum_step @{thm sum.cases(2)} @{thm sum_case_step(2)}, init = refl} n k; - -(* FIXME: because of "@ lhss", the output could contain type variables that are not in the input; - also, "fp_sort" should put the "resBs" first and in the order in which they appear *) -fun fp_sort lhss NONE Ass = Library.sort (Term_Ord.typ_ord o pairself TFree) - (subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss - | fp_sort lhss (SOME resBs) Ass = - (subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs)) @ lhss; - -fun mk_fp_bnf timer construct_fp resBs bs map_bs rel_bs set_bss sort lhss bnfs deadss livess - unfold_set lthy = - let - val name = mk_common_name (map Binding.name_of bs); - fun qualify i = - let val namei = name ^ nonzero_string_of_int i; - in Binding.qualify true namei end; - - val Ass = map (map dest_TFree) livess; - val resDs = (case resBs of NONE => [] | SOME Ts => fold (subtract (op =)) Ass Ts); - val Ds = fold (fold Term.add_tfreesT) deadss []; - - val _ = (case Library.inter (op =) Ds lhss of [] => () - | A :: _ => error ("Inadmissible type recursion (cannot take fixed point of dead type \ - \variable " ^ quote (Syntax.string_of_typ lthy (TFree A)) ^ ")")); - - val timer = time (timer "Construction of BNFs"); - - val ((kill_poss, _), (bnfs', (unfold_set', lthy'))) = - normalize_bnfs qualify Ass Ds sort bnfs unfold_set lthy; - - val Dss = map3 (append oo map o nth) livess kill_poss deadss; - - val ((bnfs'', deadss), lthy'') = - fold_map3 (seal_bnf unfold_set') (map (Binding.prefix_name preN) bs) Dss bnfs' lthy' - |>> split_list; - - val timer = time (timer "Normalization & sealing of BNFs"); - - val res = construct_fp resBs bs map_bs rel_bs set_bss (map TFree resDs, deadss) bnfs'' lthy''; - - val timer = time (timer "FP construction in total"); - in - timer; (bnfs'', res) - end; - -fun fp_bnf construct_fp bs mixfixes map_bs rel_bs set_bss resBs eqs lthy = - let - val timer = time (Timer.startRealTimer ()); - val (lhss, rhss) = split_list eqs; - val sort = fp_sort lhss (SOME resBs); - fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b)); - val ((bnfs, (Dss, Ass)), (unfold_set, lthy')) = apfst (apsnd split_list o split_list) - (fold_map2 (fn b => bnf_of_typ Smart_Inline (qualify b) sort) bs rhss - (empty_unfolds, lthy)); - in - mk_fp_bnf timer (construct_fp mixfixes) (SOME resBs) bs map_bs rel_bs set_bss sort lhss bnfs Dss - Ass unfold_set lthy' - end; - -end; diff -r 19ee0cebe76d -r 106afdf5806c src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed May 01 06:00:55 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed May 01 19:33:49 2013 +0200 @@ -11,7 +11,7 @@ {lfp: bool, index: int, pre_bnfs: BNF_Def.bnf list, - fp_res: BNF_FP.fp_result, + fp_res: BNF_FP_Util.fp_result, ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list, xxfolds: term list, xxrecs: term list, @@ -46,7 +46,7 @@ val datatypes: bool -> (mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list -> binding list list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory -> - BNF_FP.fp_result * local_theory) -> + BNF_FP_Util.fp_result * local_theory) -> (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) * ((((binding * binding) * (binding * typ) list) * (binding * term) list) * mixfix) list) list -> @@ -54,7 +54,7 @@ val parse_datatype_cmd: bool -> (mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list -> binding list list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory -> - BNF_FP.fp_result * local_theory) -> + BNF_FP_Util.fp_result * local_theory) -> (local_theory -> local_theory) parser end; @@ -64,7 +64,7 @@ open BNF_Util open BNF_Ctr_Sugar open BNF_Def -open BNF_FP +open BNF_FP_Util open BNF_FP_Def_Sugar_Tactics val EqN = "Eq_"; diff -r 19ee0cebe76d -r 106afdf5806c src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Wed May 01 06:00:55 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Wed May 01 19:33:49 2013 +0200 @@ -33,7 +33,7 @@ open BNF_Tactics open BNF_Util -open BNF_FP +open BNF_FP_Util val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)}; val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)}; diff -r 19ee0cebe76d -r 106afdf5806c src/HOL/BNF/Tools/bnf_fp_util.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Wed May 01 19:33:49 2013 +0200 @@ -0,0 +1,494 @@ +(* Title: HOL/BNF/Tools/bnf_fp_util.ML + Author: Dmitriy Traytel, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012, 2013 + +Shared library for the datatype and codatatype constructions. +*) + +signature BNF_FP_UTIL = +sig + type fp_result = + {bnfs: BNF_Def.bnf list, + ctors: term list, + dtors: term list, + folds: term list, + recs: term list, + induct: thm, + strong_induct: thm, + dtor_ctors: thm list, + ctor_dtors: thm list, + ctor_injects: thm list, + map_thms: thm list, + set_thmss: thm list list, + rel_thms: thm list, + fold_thms: thm list, + rec_thms: thm list} + + val fp_name_of_ctor: term -> string + val morph_fp_result: morphism -> fp_result -> fp_result + val eq_fp_result: fp_result * fp_result -> bool + + val time: Timer.real_timer -> string -> Timer.real_timer + + val IITN: string + val LevN: string + val algN: string + val behN: string + val bisN: string + val carTN: string + val caseN: string + val coN: string + val coinductN: string + val corecN: string + val ctorN: string + val ctor_dtorN: string + val ctor_dtor_corecN: string + val ctor_dtor_unfoldN: string + val ctor_exhaustN: string + val ctor_induct2N: string + val ctor_inductN: string + val ctor_injectN: string + val ctor_foldN: string + val ctor_fold_uniqueN: string + val ctor_mapN: string + val ctor_map_uniqueN: string + val ctor_recN: string + val ctor_rec_uniqueN: string + val ctor_relN: string + val ctor_set_inclN: string + val ctor_set_set_inclN: string + val ctor_srelN: string + val disc_unfoldN: string + val disc_unfold_iffN: string + val disc_corecN: string + val disc_corec_iffN: string + val dtorN: string + val dtor_coinductN: string + val dtor_corecN: string + val dtor_corec_uniqueN: string + val dtor_ctorN: string + val dtor_exhaustN: string + val dtor_injectN: string + val dtor_mapN: string + val dtor_map_coinductN: string + val dtor_map_strong_coinductN: string + val dtor_map_uniqueN: string + val dtor_relN: string + val dtor_set_inclN: string + val dtor_set_set_inclN: string + val dtor_srelN: string + val dtor_srel_coinductN: string + val dtor_srel_strong_coinductN: string + val dtor_strong_coinductN: string + val dtor_unfoldN: string + val dtor_unfold_uniqueN: string + val exhaustN: string + val foldN: string + val hsetN: string + val hset_recN: string + val inductN: string + val injectN: string + val isNodeN: string + val lsbisN: string + val mapN: string + val map_uniqueN: string + val min_algN: string + val morN: string + val nchotomyN: string + val recN: string + val rel_injectN: string + val rel_distinctN: string + val rvN: string + val sel_corecN: string + val set_inclN: string + val set_set_inclN: string + val sel_unfoldN: string + val setsN: string + val simpsN: string + val strTN: string + val str_initN: string + val strong_coinductN: string + val sum_bdN: string + val sum_bdTN: string + val unfoldN: string + val uniqueN: string + + (* TODO: Don't index set facts. Isabelle packages traditionally generate uniform names. *) + val mk_ctor_setN: int -> string + val mk_dtor_setN: int -> string + val mk_dtor_set_inductN: int -> string + val mk_set_inductN: int -> string + + val mk_common_name: string list -> string + + val split_conj_thm: thm -> thm list + val split_conj_prems: int -> thm -> thm + + val mk_sumTN: typ list -> typ + val mk_sumTN_balanced: typ list -> typ + + val id_const: typ -> term + + val Inl_const: typ -> typ -> term + val Inr_const: typ -> typ -> term + + val mk_Inl: typ -> term -> term + val mk_Inr: typ -> term -> term + val mk_InN: typ list -> term -> int -> term + val mk_InN_balanced: typ -> int -> term -> int -> term + val mk_sum_case: term * term -> term + val mk_sum_caseN: term list -> term + val mk_sum_caseN_balanced: term list -> term + + val dest_sumT: typ -> typ * typ + val dest_sumTN: int -> typ -> typ list + val dest_sumTN_balanced: int -> typ -> typ list + val dest_tupleT: int -> typ -> typ list + + val mk_Field: term -> term + val mk_If: term -> term -> term -> term + val mk_union: term * term -> term + + val mk_sumEN: int -> thm + val mk_sumEN_balanced: int -> thm + val mk_sumEN_tupled_balanced: int list -> thm + val mk_sum_casesN: int -> int -> thm + val mk_sum_casesN_balanced: int -> int -> thm + + val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list + + val fp_bnf: (mixfix list -> (string * sort) list option -> binding list -> binding list -> + binding list -> binding list list -> typ list * typ list list -> BNF_Def.bnf list -> + local_theory -> 'a) -> + binding list -> mixfix list -> binding list -> binding list -> binding list list -> + (string * sort) list -> ((string * sort) * typ) list -> local_theory -> BNF_Def.bnf list * 'a +end; + +structure BNF_FP_Util : BNF_FP_UTIL = +struct + +open BNF_Comp +open BNF_Def +open BNF_Util + +type fp_result = + {bnfs: BNF_Def.bnf list, + ctors: term list, + dtors: term list, + folds: term list, + recs: term list, + induct: thm, + strong_induct: thm, + dtor_ctors: thm list, + ctor_dtors: thm list, + ctor_injects: thm list, + map_thms: thm list, + set_thmss: thm list list, + rel_thms: thm list, + fold_thms: thm list, + rec_thms: thm list}; + +val fp_name_of_ctor = fst o dest_Type o range_type o fastype_of; + +fun morph_fp_result phi {bnfs, ctors, dtors, folds, recs, induct, strong_induct, dtor_ctors, + ctor_dtors, ctor_injects, map_thms, set_thmss, rel_thms, fold_thms, rec_thms} = + {bnfs = map (morph_bnf phi) bnfs, + ctors = map (Morphism.term phi) ctors, + dtors = map (Morphism.term phi) dtors, + folds = map (Morphism.term phi) folds, + recs = map (Morphism.term phi) recs, + induct = Morphism.thm phi induct, + strong_induct = Morphism.thm phi strong_induct, + dtor_ctors = map (Morphism.thm phi) dtor_ctors, + ctor_dtors = map (Morphism.thm phi) ctor_dtors, + ctor_injects = map (Morphism.thm phi) ctor_injects, + map_thms = map (Morphism.thm phi) map_thms, + set_thmss = map (map (Morphism.thm phi)) set_thmss, + rel_thms = map (Morphism.thm phi) rel_thms, + fold_thms = map (Morphism.thm phi) fold_thms, + rec_thms = map (Morphism.thm phi) rec_thms}; + +fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) = + eq_list eq_bnf (bnfs1, bnfs2); + +val timing = true; +fun time timer msg = (if timing + then warning (msg ^ ": " ^ ATP_Util.string_from_time (Timer.checkRealTimer timer)) + else (); Timer.startRealTimer ()); + +val preN = "pre_" +val rawN = "raw_" + +val coN = "co" +val unN = "un" +val algN = "alg" +val IITN = "IITN" +val foldN = "fold" +val unfoldN = unN ^ foldN +val uniqueN = "_unique" +val simpsN = "simps" +val ctorN = "ctor" +val dtorN = "dtor" +val ctor_foldN = ctorN ^ "_" ^ foldN +val dtor_unfoldN = dtorN ^ "_" ^ unfoldN +val ctor_fold_uniqueN = ctor_foldN ^ uniqueN +val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN +val ctor_dtor_unfoldN = ctorN ^ "_" ^ dtor_unfoldN +val ctor_mapN = ctorN ^ "_" ^ mapN +val dtor_mapN = dtorN ^ "_" ^ mapN +val map_uniqueN = mapN ^ uniqueN +val ctor_map_uniqueN = ctorN ^ "_" ^ map_uniqueN +val dtor_map_uniqueN = dtorN ^ "_" ^ map_uniqueN +val min_algN = "min_alg" +val morN = "mor" +val bisN = "bis" +val lsbisN = "lsbis" +val sum_bdTN = "sbdT" +val sum_bdN = "sbd" +val carTN = "carT" +val strTN = "strT" +val isNodeN = "isNode" +val LevN = "Lev" +val rvN = "recover" +val behN = "beh" +val setsN = "sets" +val mk_ctor_setN = prefix (ctorN ^ "_") o mk_setN +val mk_dtor_setN = prefix (dtorN ^ "_") o mk_setN +fun mk_set_inductN i = mk_setN i ^ "_induct" +val mk_dtor_set_inductN = prefix (dtorN ^ "_") o mk_set_inductN + +val str_initN = "str_init" +val recN = "rec" +val corecN = coN ^ recN +val ctor_recN = ctorN ^ "_" ^ recN +val ctor_rec_uniqueN = ctor_recN ^ uniqueN +val dtor_corecN = dtorN ^ "_" ^ corecN +val dtor_corec_uniqueN = dtor_corecN ^ uniqueN +val ctor_dtor_corecN = ctorN ^ "_" ^ dtor_corecN + +val ctor_dtorN = ctorN ^ "_" ^ dtorN +val dtor_ctorN = dtorN ^ "_" ^ ctorN +val nchotomyN = "nchotomy" +val injectN = "inject" +val exhaustN = "exhaust" +val ctor_injectN = ctorN ^ "_" ^ injectN +val ctor_exhaustN = ctorN ^ "_" ^ exhaustN +val dtor_injectN = dtorN ^ "_" ^ injectN +val dtor_exhaustN = dtorN ^ "_" ^ exhaustN +val ctor_relN = ctorN ^ "_" ^ relN +val dtor_relN = dtorN ^ "_" ^ relN +val ctor_srelN = ctorN ^ "_" ^ srelN +val dtor_srelN = dtorN ^ "_" ^ srelN +val inductN = "induct" +val coinductN = coN ^ inductN +val ctor_inductN = ctorN ^ "_" ^ inductN +val ctor_induct2N = ctor_inductN ^ "2" +val dtor_map_coinductN = dtor_mapN ^ "_" ^ coinductN +val dtor_coinductN = dtorN ^ "_" ^ coinductN +val dtor_srel_coinductN = dtor_srelN ^ "_" ^ coinductN +val strong_coinductN = "strong_" ^ coinductN +val dtor_map_strong_coinductN = dtor_mapN ^ "_" ^ strong_coinductN +val dtor_strong_coinductN = dtorN ^ "_" ^ strong_coinductN +val dtor_srel_strong_coinductN = dtor_srelN ^ "_" ^ strong_coinductN +val hsetN = "Hset" +val hset_recN = hsetN ^ "_rec" +val set_inclN = "set_incl" +val ctor_set_inclN = ctorN ^ "_" ^ set_inclN +val dtor_set_inclN = dtorN ^ "_" ^ set_inclN +val set_set_inclN = "set_set_incl" +val ctor_set_set_inclN = ctorN ^ "_" ^ set_set_inclN +val dtor_set_set_inclN = dtorN ^ "_" ^ set_set_inclN + +val caseN = "case" +val discN = "disc" +val disc_unfoldN = discN ^ "_" ^ unfoldN +val disc_corecN = discN ^ "_" ^ corecN +val iffN = "_iff" +val disc_unfold_iffN = discN ^ "_" ^ unfoldN ^ iffN +val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN +val distinctN = "distinct" +val rel_distinctN = relN ^ "_" ^ distinctN +val injectN = "inject" +val rel_injectN = relN ^ "_" ^ injectN +val selN = "sel" +val sel_unfoldN = selN ^ "_" ^ unfoldN +val sel_corecN = selN ^ "_" ^ corecN + +val mk_common_name = space_implode "_"; + +fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T'); + +fun dest_sumTN 1 T = [T] + | dest_sumTN n (Type (@{type_name sum}, [T, T'])) = T :: dest_sumTN (n - 1) T'; + +val dest_sumTN_balanced = Balanced_Tree.dest dest_sumT; + +(* TODO: move something like this to "HOLogic"? *) +fun dest_tupleT 0 @{typ unit} = [] + | dest_tupleT 1 T = [T] + | dest_tupleT n (Type (@{type_name prod}, [T, T'])) = T :: dest_tupleT (n - 1) T'; + +val mk_sumTN = Library.foldr1 mk_sumT; +val mk_sumTN_balanced = Balanced_Tree.make mk_sumT; + +fun id_const T = Const (@{const_name id}, T --> T); + +fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT)); +fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t; + +fun Inr_const LT RT = Const (@{const_name Inr}, RT --> mk_sumT (LT, RT)); +fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t; + +fun mk_InN [_] t 1 = t + | mk_InN (_ :: Ts) t 1 = mk_Inl (mk_sumTN Ts) t + | mk_InN (LT :: Ts) t m = mk_Inr LT (mk_InN Ts t (m - 1)) + | mk_InN Ts t _ = raise (TYPE ("mk_InN", Ts, [t])); + +fun mk_InN_balanced sum_T n t k = + let + fun repair_types T (Const (s as @{const_name Inl}, _) $ t) = repair_inj_types T s fst t + | repair_types T (Const (s as @{const_name Inr}, _) $ t) = repair_inj_types T s snd t + | repair_types _ t = t + and repair_inj_types T s get t = + let val T' = get (dest_sumT T) in + Const (s, T' --> T) $ repair_types T' t + end; + in + Balanced_Tree.access {left = mk_Inl dummyT, right = mk_Inr dummyT, init = t} n k + |> repair_types sum_T + end; + +fun mk_sum_case (f, g) = + let + val fT = fastype_of f; + val gT = fastype_of g; + in + Const (@{const_name sum_case}, + fT --> gT --> mk_sumT (domain_type fT, domain_type gT) --> range_type fT) $ f $ g + end; + +val mk_sum_caseN = Library.foldr1 mk_sum_case; +val mk_sum_caseN_balanced = Balanced_Tree.make mk_sum_case; + +fun mk_If p t f = + let val T = fastype_of t; + in Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ p $ t $ f end; + +fun mk_Field r = + let val T = fst (dest_relT (fastype_of r)); + in Const (@{const_name Field}, mk_relT (T, T) --> HOLogic.mk_setT T) $ r end; + +val mk_union = HOLogic.mk_binop @{const_name sup}; + +(*dangerous; use with monotonic, converging functions only!*) +fun fixpoint eq f X = if subset eq (f X, X) then X else fixpoint eq f (f X); + +(* stolen from "~~/src/HOL/Tools/Datatype/datatype_aux.ML" *) +fun split_conj_thm th = + ((th RS conjunct1) :: split_conj_thm (th RS conjunct2)) handle THM _ => [th]; + +fun split_conj_prems limit th = + let + fun split n i th = + if i = n then th else split n (i + 1) (conjI RSN (i, th)) handle THM _ => th; + in split limit 1 th end; + +fun mk_sumEN 1 = @{thm one_pointE} + | mk_sumEN 2 = @{thm sumE} + | mk_sumEN n = + (fold (fn i => fn thm => @{thm obj_sum_step} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF + replicate n (impI RS allI); + +fun mk_obj_sumEN_balanced n = + Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f}))) + (replicate n asm_rl); + +fun mk_sumEN_balanced' n all_impIs = mk_obj_sumEN_balanced n OF all_impIs RS @{thm obj_one_pointE}; + +fun mk_sumEN_balanced 1 = @{thm one_pointE} (*optimization*) + | mk_sumEN_balanced 2 = @{thm sumE} (*optimization*) + | mk_sumEN_balanced n = mk_sumEN_balanced' n (replicate n (impI RS allI)); + +fun mk_tupled_allIN 0 = @{thm unit_all_impI} + | mk_tupled_allIN 1 = @{thm impI[THEN allI]} + | mk_tupled_allIN 2 = @{thm prod_all_impI} (*optimization*) + | mk_tupled_allIN n = mk_tupled_allIN (n - 1) RS @{thm prod_all_impI_step}; + +fun mk_sumEN_tupled_balanced ms = + let val n = length ms in + if forall (curry (op =) 1) ms then mk_sumEN_balanced n + else mk_sumEN_balanced' n (map mk_tupled_allIN ms) + end; + +fun mk_sum_casesN 1 1 = refl + | mk_sum_casesN _ 1 = @{thm sum.cases(1)} + | mk_sum_casesN 2 2 = @{thm sum.cases(2)} + | mk_sum_casesN n k = trans OF [@{thm sum_case_step(2)}, mk_sum_casesN (n - 1) (k - 1)]; + +fun mk_sum_step base step thm = + if Thm.eq_thm_prop (thm, refl) then base else trans OF [step, thm]; + +fun mk_sum_casesN_balanced 1 1 = refl + | mk_sum_casesN_balanced n k = + Balanced_Tree.access {left = mk_sum_step @{thm sum.cases(1)} @{thm sum_case_step(1)}, + right = mk_sum_step @{thm sum.cases(2)} @{thm sum_case_step(2)}, init = refl} n k; + +(* FIXME: because of "@ lhss", the output could contain type variables that are not in the input; + also, "fp_sort" should put the "resBs" first and in the order in which they appear *) +fun fp_sort lhss NONE Ass = Library.sort (Term_Ord.typ_ord o pairself TFree) + (subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss + | fp_sort lhss (SOME resBs) Ass = + (subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs)) @ lhss; + +fun mk_fp_bnf timer construct_fp resBs bs map_bs rel_bs set_bss sort lhss bnfs deadss livess + unfold_set lthy = + let + val name = mk_common_name (map Binding.name_of bs); + fun qualify i = + let val namei = name ^ nonzero_string_of_int i; + in Binding.qualify true namei end; + + val Ass = map (map dest_TFree) livess; + val resDs = (case resBs of NONE => [] | SOME Ts => fold (subtract (op =)) Ass Ts); + val Ds = fold (fold Term.add_tfreesT) deadss []; + + val _ = (case Library.inter (op =) Ds lhss of [] => () + | A :: _ => error ("Inadmissible type recursion (cannot take fixed point of dead type \ + \variable " ^ quote (Syntax.string_of_typ lthy (TFree A)) ^ ")")); + + val timer = time (timer "Construction of BNFs"); + + val ((kill_poss, _), (bnfs', (unfold_set', lthy'))) = + normalize_bnfs qualify Ass Ds sort bnfs unfold_set lthy; + + val Dss = map3 (append oo map o nth) livess kill_poss deadss; + + val ((bnfs'', deadss), lthy'') = + fold_map3 (seal_bnf unfold_set') (map (Binding.prefix_name preN) bs) Dss bnfs' lthy' + |>> split_list; + + val timer = time (timer "Normalization & sealing of BNFs"); + + val res = construct_fp resBs bs map_bs rel_bs set_bss (map TFree resDs, deadss) bnfs'' lthy''; + + val timer = time (timer "FP construction in total"); + in + timer; (bnfs'', res) + end; + +fun fp_bnf construct_fp bs mixfixes map_bs rel_bs set_bss resBs eqs lthy = + let + val timer = time (Timer.startRealTimer ()); + val (lhss, rhss) = split_list eqs; + val sort = fp_sort lhss (SOME resBs); + fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b)); + val ((bnfs, (Dss, Ass)), (unfold_set, lthy')) = apfst (apsnd split_list o split_list) + (fold_map2 (fn b => bnf_of_typ Smart_Inline (qualify b) sort) bs rhss + (empty_unfolds, lthy)); + in + mk_fp_bnf timer (construct_fp mixfixes) (SOME resBs) bs map_bs rel_bs set_bss sort lhss bnfs Dss + Ass unfold_set lthy' + end; + +end; diff -r 19ee0cebe76d -r 106afdf5806c src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Wed May 01 06:00:55 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Wed May 01 19:33:49 2013 +0200 @@ -11,7 +11,7 @@ sig val construct_gfp: mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list -> binding list list -> typ list * typ list list -> BNF_Def.bnf list -> - local_theory -> BNF_FP.fp_result * local_theory + local_theory -> BNF_FP_Util.fp_result * local_theory end; structure BNF_GFP : BNF_GFP = @@ -21,7 +21,7 @@ open BNF_Util open BNF_Tactics open BNF_Comp -open BNF_FP +open BNF_FP_Util open BNF_FP_Def_Sugar open BNF_GFP_Util open BNF_GFP_Tactics diff -r 19ee0cebe76d -r 106afdf5806c src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Wed May 01 06:00:55 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Wed May 01 19:33:49 2013 +0200 @@ -131,7 +131,7 @@ open BNF_Tactics open BNF_Util -open BNF_FP +open BNF_FP_Util open BNF_GFP_Util val fst_convol_fun_cong_sym = @{thm fst_convol} RS fun_cong RS sym; diff -r 19ee0cebe76d -r 106afdf5806c src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Wed May 01 06:00:55 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Wed May 01 19:33:49 2013 +0200 @@ -10,7 +10,7 @@ sig val construct_lfp: mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list -> binding list list -> typ list * typ list list -> BNF_Def.bnf list -> - local_theory -> BNF_FP.fp_result * local_theory + local_theory -> BNF_FP_Util.fp_result * local_theory end; structure BNF_LFP : BNF_LFP = @@ -20,7 +20,7 @@ open BNF_Util open BNF_Tactics open BNF_Comp -open BNF_FP +open BNF_FP_Util open BNF_FP_Def_Sugar open BNF_LFP_Util open BNF_LFP_Tactics