respect order of/additional type variables supplied by the user in fixed point constructions;
authortraytel
Thu Sep 06 16:06:22 2012 +0200 (2012-09-06)
changeset 49185073d7d1b7488
parent 49184 83fdea0c4779
child 49186 4b5fa9d5e330
respect order of/additional type variables supplied by the user in fixed point constructions;
src/HOL/Codatatype/Examples/Misc_Codata.thy
src/HOL/Codatatype/Examples/Misc_Data.thy
src/HOL/Codatatype/Tools/bnf_comp.ML
src/HOL/Codatatype/Tools/bnf_fp_util.ML
src/HOL/Codatatype/Tools/bnf_gfp.ML
src/HOL/Codatatype/Tools/bnf_lfp.ML
     1.1 --- a/src/HOL/Codatatype/Examples/Misc_Codata.thy	Thu Sep 06 12:21:33 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Examples/Misc_Codata.thy	Thu Sep 06 16:06:22 2012 +0200
     1.3 @@ -53,15 +53,10 @@
     1.4     and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
     1.5     and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
     1.6  
     1.7 -codata_raw some_killing: 'A = "'a \<Rightarrow> 'b \<Rightarrow> ('A + 'B)"
     1.8 -       and in_here: 'B = "'b \<times> 'a + 'c"
     1.9 -
    1.10 -(* FIXME
    1.11  codata ('a, 'b, 'c) some_killing =
    1.12    SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here"
    1.13 - and ('a, 'b, 'c) in_here =
    1.14 +   and ('a, 'b, 'c) in_here =
    1.15    IH1 'b 'a | IH2 'c
    1.16 -*)
    1.17  
    1.18  codata_raw some_killing': 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)"
    1.19  and in_here': 'c = "'d + 'e"
    1.20 @@ -69,7 +64,7 @@
    1.21  codata_raw some_killing'': 'a = "'b \<Rightarrow> 'c"
    1.22  and in_here'': 'c = "'d \<times> 'b + 'e"
    1.23  
    1.24 -codata_raw less_killing: 'a = "'b \<Rightarrow> 'c"
    1.25 +codata ('b, 'c) less_killing = LK "'b \<Rightarrow> 'c"
    1.26  
    1.27  codata 'b cps = CPS1 'b | CPS2 "'b \<Rightarrow> 'b cps"
    1.28  
    1.29 @@ -95,6 +90,14 @@
    1.30     and ('c, 'e, 'g) ind_wit =
    1.31         IW1 | IW2 'c
    1.32  
    1.33 +codata ('b, 'a) bar = BAR "'a \<Rightarrow> 'b"
    1.34 +codata ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \<Rightarrow> 'c + 'a"
    1.35 +
    1.36 +codata 'a dead_foo = A
    1.37 +(* FIXME: handle unknown type constructors using DEADID?
    1.38 +codata ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
    1.39 +*)
    1.40 +
    1.41  (* SLOW, MEMORY-HUNGRY
    1.42  codata ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list"
    1.43     and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list"
     2.1 --- a/src/HOL/Codatatype/Examples/Misc_Data.thy	Thu Sep 06 12:21:33 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Examples/Misc_Data.thy	Thu Sep 06 16:06:22 2012 +0200
     2.3 @@ -51,15 +51,10 @@
     2.4   and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
     2.5   and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
     2.6  
     2.7 -data_raw some_killing: 'A = "'a \<Rightarrow> 'b \<Rightarrow> ('A + 'B)"
     2.8 -     and in_here: 'B = "'b \<times> 'a + 'c"
     2.9 -
    2.10 -(* FIXME
    2.11  data ('a, 'b, 'c) some_killing =
    2.12    SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here"
    2.13   and ('a, 'b, 'c) in_here =
    2.14    IH1 'b 'a | IH2 'c
    2.15 -*)
    2.16  
    2.17  data 'b nofail1 = NF11 "'b nofail1 \<times> 'b" | NF12 'b
    2.18  data 'b nofail2 = NF2 "('b nofail2 \<times> 'b \<times> 'b nofail2 \<times> 'b) list"
    2.19 @@ -150,4 +145,11 @@
    2.20   and s8 = S8 nat
    2.21  *)
    2.22  
    2.23 +data ('a, 'b) bar = BAR "'b \<Rightarrow> 'a"
    2.24 +data ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \<Rightarrow> 'c + 'a"
    2.25 +
    2.26 +data 'a dead_foo = A
    2.27 +(* FIXME: handle unknown type constructors using DEADID?
    2.28 +data ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
    2.29 +*)
    2.30  end
     3.1 --- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Sep 06 12:21:33 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Sep 06 16:06:22 2012 +0200
     3.3 @@ -23,7 +23,7 @@
     3.4      (''a list list -> ''a list) -> BNF_Def.BNF list -> unfold_thms -> Proof.context ->
     3.5      (int list list * ''a list) * (BNF_Def.BNF list * (unfold_thms * Proof.context))
     3.6    val seal_bnf: unfold_thms -> binding -> typ list -> BNF_Def.BNF -> Proof.context ->
     3.7 -    BNF_Def.BNF * local_theory
     3.8 +    (BNF_Def.BNF * typ list) * local_theory
     3.9  end;
    3.10  
    3.11  structure BNF_Comp : BNF_COMP =
    3.12 @@ -656,6 +656,7 @@
    3.13      val bd_repT = fst (dest_relT (fastype_of bnf_bd));
    3.14      val bdT_bind = Binding.suffix_name ("_" ^ bdTN) b;
    3.15      val params = fold Term.add_tfreesT Ds [];
    3.16 +    val deads = map TFree params;
    3.17  
    3.18      val ((bdT_name, (bdT_glob_info, bdT_loc_info)), (lthy', lthy)) =
    3.19        lthy
    3.20 @@ -666,7 +667,7 @@
    3.21      val phi = Proof_Context.export_morphism lthy lthy';
    3.22  
    3.23      val bnf_bd' = mk_dir_image bnf_bd
    3.24 -      (Const (#Abs_name bdT_glob_info, bd_repT --> Type (bdT_name, map TFree params)))
    3.25 +      (Const (#Abs_name bdT_glob_info, bd_repT --> Type (bdT_name, deads)))
    3.26  
    3.27      val set_def = Morphism.thm phi (the (#set_def bdT_loc_info));
    3.28      val Abs_inject = Morphism.thm phi (#Abs_inject bdT_loc_info);
    3.29 @@ -701,8 +702,8 @@
    3.30  
    3.31      fun wit_tac _ = mk_simple_wit_tac (map unfold_defs (wit_thms_of_bnf bnf));
    3.32  
    3.33 -    val (bnf', lthy') = bnf_def Hardly_Inline (K Derive_All_Facts) I tacs wit_tac NONE
    3.34 -        ((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits) lthy;
    3.35 +    val (bnf', lthy') = bnf_def Hardly_Inline (K Derive_All_Facts) I tacs wit_tac (SOME deads)
    3.36 +      ((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits) lthy;
    3.37  
    3.38      val defs' = filter_refl (map_def_of_bnf bnf' :: set_defs_of_bnf bnf');
    3.39      val unfold_defs' = unfold_defs o Local_Defs.unfold lthy' defs';
    3.40 @@ -723,7 +724,7 @@
    3.41        |> map (fn (thmN, thms) =>
    3.42          ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
    3.43    in
    3.44 -    (bnf', lthy' |> Local_Theory.notes notes |> snd)
    3.45 +    ((bnf', deads), lthy' |> Local_Theory.notes notes |> snd)
    3.46    end;
    3.47  
    3.48  fun bnf_of_typ _ _ _ _ (T as TFree _) (unfold, lthy) =
     4.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Thu Sep 06 12:21:33 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Thu Sep 06 16:06:22 2012 +0200
     4.3 @@ -103,12 +103,12 @@
     4.4  
     4.5    val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
     4.6  
     4.7 -  val fp_bnf: (binding list -> mixfix list -> (string * sort) list -> typ list list ->
     4.8 -    BNF_Def.BNF list -> local_theory -> 'a) ->
     4.9 +  val fp_bnf: (mixfix list -> (string * sort) list option -> binding list ->
    4.10 +    typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) ->
    4.11      binding list -> mixfix list -> (string * sort) list -> ((string * sort) * typ) list ->
    4.12      local_theory -> 'a
    4.13 -  val fp_bnf_cmd: (binding list -> mixfix list -> (string * sort) list -> typ list list ->
    4.14 -    BNF_Def.BNF list -> local_theory -> 'a) ->
    4.15 +  val fp_bnf_cmd: (mixfix list -> (string * sort) list option -> binding list ->
    4.16 +    typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) ->
    4.17      binding list * (string list * string list) -> local_theory -> 'a
    4.18  end;
    4.19  
    4.20 @@ -272,10 +272,12 @@
    4.21  
    4.22  (* FIXME: because of "@ lhss", the output could contain type variables that are not in the input;
    4.23     also, "fp_sort" should put the "resBs" first and in the order in which they appear *)
    4.24 -fun fp_sort lhss Ass = Library.sort (Term_Ord.typ_ord o pairself TFree)
    4.25 -  (subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss;
    4.26 +fun fp_sort lhss NONE Ass = Library.sort (Term_Ord.typ_ord o pairself TFree)
    4.27 +    (subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss
    4.28 +  | fp_sort lhss (SOME resBs) Ass =
    4.29 +    (subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs)) @ lhss;
    4.30  
    4.31 -fun mk_fp_bnf timer construct bs mixfixes resBs sort lhss bnfs deadss livess unfold lthy =
    4.32 +fun mk_fp_bnf timer construct resBs bs sort lhss bnfs deadss livess unfold lthy =
    4.33    let
    4.34      val name = fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "";
    4.35      fun qualify i bind =
    4.36 @@ -286,8 +288,8 @@
    4.37        end;
    4.38  
    4.39      val Ass = map (map dest_TFree) livess;
    4.40 -    val resDs = fold (subtract (op =)) Ass resBs;
    4.41 -    val Ds = fold (fold Term.add_tfreesT) deadss resDs;
    4.42 +    val resDs = (case resBs of NONE => [] | SOME Ts => fold (subtract (op =)) Ass Ts);
    4.43 +    val Ds = fold (fold Term.add_tfreesT) deadss [];
    4.44  
    4.45      val _ = (case Library.inter (op =) Ds lhss of [] => ()
    4.46        | A :: _ => error ("Nonadmissible type recursion (cannot take fixed point of dead type \
    4.47 @@ -300,12 +302,13 @@
    4.48  
    4.49      val Dss = map3 (append oo map o nth) livess kill_poss deadss;
    4.50  
    4.51 -    val (bnfs'', lthy'') =
    4.52 -      fold_map3 (seal_bnf unfold') (map (Binding.suffix_name "BNF") bs) Dss bnfs' lthy';
    4.53 +    val ((bnfs'', deadss), lthy'') =
    4.54 +      fold_map3 (seal_bnf unfold') (map (Binding.suffix_name "BNF") bs) Dss bnfs' lthy'
    4.55 +      |>> split_list;
    4.56  
    4.57      val timer = time (timer "Normalization & sealing of BNFs");
    4.58  
    4.59 -    val res = construct bs mixfixes resDs Dss bnfs'' lthy'';
    4.60 +    val res = construct resBs bs (map TFree resDs, deadss) bnfs'' lthy'';
    4.61  
    4.62      val timer = time (timer "FP construction in total");
    4.63    in
    4.64 @@ -316,25 +319,25 @@
    4.65    let
    4.66      val timer = time (Timer.startRealTimer ());
    4.67      val (lhss, rhss) = split_list eqs;
    4.68 -    val sort = fp_sort lhss;
    4.69 +    val sort = fp_sort lhss (SOME resBs);
    4.70      val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list)
    4.71        (fold_map2 (fn b => bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort) bs rhss
    4.72          (empty_unfold, lthy));
    4.73    in
    4.74 -    mk_fp_bnf timer construct bs mixfixes resBs sort lhss bnfs Dss Ass unfold lthy'
    4.75 +    mk_fp_bnf timer (construct mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold lthy'
    4.76    end;
    4.77  
    4.78  fun fp_bnf_cmd construct (bs, (raw_lhss, raw_bnfs)) lthy =
    4.79    let
    4.80      val timer = time (Timer.startRealTimer ());
    4.81      val lhss = map (dest_TFree o Syntax.read_typ lthy) raw_lhss;
    4.82 -    val sort = fp_sort lhss;
    4.83 +    val sort = fp_sort lhss NONE;
    4.84      val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list)
    4.85        (fold_map2 (fn b => fn rawT =>
    4.86          (bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort (Syntax.read_typ lthy rawT)))
    4.87 -        bs raw_bnfs (empty_unfold, lthy));
    4.88 +      bs raw_bnfs (empty_unfold, lthy));
    4.89    in
    4.90 -    mk_fp_bnf timer construct bs (map (K NoSyn) bs) [] sort lhss bnfs Dss Ass unfold lthy'
    4.91 +    mk_fp_bnf timer (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold lthy'
    4.92    end;
    4.93  
    4.94  end;
     5.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Thu Sep 06 12:21:33 2012 +0200
     5.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Thu Sep 06 16:06:22 2012 +0200
     5.3 @@ -9,8 +9,8 @@
     5.4  
     5.5  signature BNF_GFP =
     5.6  sig
     5.7 -  val bnf_gfp: binding list -> mixfix list -> (string * sort) list -> typ list list ->
     5.8 -    BNF_Def.BNF list -> local_theory ->
     5.9 +  val bnf_gfp: mixfix list -> (string * sort) list option -> binding list ->
    5.10 +    typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
    5.11      (term list * term list * term list * term list * thm list * thm list * thm list) * local_theory
    5.12  end;
    5.13  
    5.14 @@ -53,7 +53,7 @@
    5.15       ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
    5.16  
    5.17  (*all bnfs have the same lives*)
    5.18 -fun bnf_gfp bs mixfixes resDs Dss_insts bnfs lthy =
    5.19 +fun bnf_gfp mixfixes resBs bs (resDs, Dss) bnfs lthy =
    5.20    let
    5.21      val timer = time (Timer.startRealTimer ());
    5.22  
    5.23 @@ -66,8 +66,7 @@
    5.24  
    5.25      (* TODO: check if m, n etc are sane *)
    5.26  
    5.27 -    val Dss = map (fn Ds => map TFree (fold Term.add_tfreesT Ds [])) Dss_insts;
    5.28 -    val deads = fold (union (op =)) Dss (map TFree resDs);
    5.29 +    val deads = fold (union (op =)) Dss resDs;
    5.30      val names_lthy = fold Variable.declare_typ deads lthy;
    5.31  
    5.32      (* tvars *)
    5.33 @@ -92,8 +91,16 @@
    5.34      val Css' = replicate n allCs';
    5.35  
    5.36      (* typs *)
    5.37 +    val dead_poss =
    5.38 +      (case resBs of
    5.39 +        NONE => map SOME deads @ replicate m NONE
    5.40 +      | SOME Ts => map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) Ts);
    5.41 +    fun mk_param NONE passive = (hd passive, tl passive)
    5.42 +      | mk_param (SOME a) passive = (a, passive);
    5.43 +    val mk_params = fold_map mk_param dead_poss #> fst;
    5.44 +
    5.45      fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs;
    5.46 -    val (params, params') = `(map Term.dest_TFree) (deads @ passiveAs);
    5.47 +    val (params, params') = `(map Term.dest_TFree) (mk_params passiveAs);
    5.48      val FTsAs = mk_FTs allAs;
    5.49      val FTsBs = mk_FTs allBs;
    5.50      val FTsCs = mk_FTs allCs;
    5.51 @@ -1912,7 +1919,7 @@
    5.52      (*transforms defined frees into consts*)
    5.53      val phi = Proof_Context.export_morphism lthy_old lthy;
    5.54      fun mk_unfs passive =
    5.55 -      map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (deads @ passive)) o
    5.56 +      map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o
    5.57          Morphism.term phi) unf_frees;
    5.58      val unfs = mk_unfs passiveAs;
    5.59      val unf's = mk_unfs passiveBs;
     6.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Thu Sep 06 12:21:33 2012 +0200
     6.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Thu Sep 06 16:06:22 2012 +0200
     6.3 @@ -8,8 +8,8 @@
     6.4  
     6.5  signature BNF_LFP =
     6.6  sig
     6.7 -  val bnf_lfp: binding list -> mixfix list -> (string * sort) list -> typ list list ->
     6.8 -    BNF_Def.BNF list -> local_theory ->
     6.9 +  val bnf_lfp:  mixfix list -> (string * sort) list option -> binding list ->
    6.10 +    typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
    6.11      (term list * term list * term list * term list * thm list * thm list * thm list) * local_theory
    6.12  end;
    6.13  
    6.14 @@ -24,7 +24,7 @@
    6.15  open BNF_LFP_Tactics
    6.16  
    6.17  (*all bnfs have the same lives*)
    6.18 -fun bnf_lfp bs mixfixes resDs Dss_insts bnfs lthy =
    6.19 +fun bnf_lfp mixfixes resBs bs (resDs, Dss) bnfs lthy =
    6.20    let
    6.21      val timer = time (Timer.startRealTimer ());
    6.22      val live = live_of_bnf (hd bnfs);
    6.23 @@ -35,8 +35,7 @@
    6.24  
    6.25      (* TODO: check if m, n etc are sane *)
    6.26  
    6.27 -    val Dss = map (fn Ds => map TFree (fold Term.add_tfreesT Ds [])) Dss_insts;
    6.28 -    val deads = fold (union (op =)) Dss (map TFree resDs);
    6.29 +    val deads = fold (union (op =)) Dss resDs;
    6.30      val names_lthy = fold Variable.declare_typ deads lthy;
    6.31  
    6.32      (* tvars *)
    6.33 @@ -58,8 +57,16 @@
    6.34      val Css' = replicate n allCs';
    6.35  
    6.36      (* typs *)
    6.37 +    val dead_poss =
    6.38 +      (case resBs of
    6.39 +        NONE => map SOME deads @ replicate m NONE
    6.40 +      | SOME Ts => map (fn T => if member (op =) deads (TFree T) then SOME (TFree T) else NONE) Ts);
    6.41 +    fun mk_param NONE passive = (hd passive, tl passive)
    6.42 +      | mk_param (SOME a) passive = (a, passive);
    6.43 +    val mk_params = fold_map mk_param dead_poss #> fst;
    6.44 +
    6.45      fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs;
    6.46 -    val (params, params') = `(map Term.dest_TFree) (deads @ passiveAs);
    6.47 +    val (params, params') = `(map Term.dest_TFree) (mk_params passiveAs);
    6.48      val FTsAs = mk_FTs allAs;
    6.49      val FTsBs = mk_FTs allBs;
    6.50      val FTsCs = mk_FTs allCs;
    6.51 @@ -1019,7 +1026,7 @@
    6.52      (*transforms defined frees into consts*)
    6.53      val phi = Proof_Context.export_morphism lthy_old lthy;
    6.54      fun mk_flds passive =
    6.55 -      map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (deads @ passive)) o
    6.56 +      map (Term.subst_atomic_types (map (Morphism.typ phi) params' ~~ (mk_params passive)) o
    6.57          Morphism.term phi) fld_frees;
    6.58      val flds = mk_flds passiveAs;
    6.59      val fld's = mk_flds passiveBs;