src/HOLCF/Tools/fixrec.ML
changeset 33671 4b0f2599ed48
parent 33670 02b7738aef6a
child 33726 0878aecbf119
equal deleted inserted replaced
33670:02b7738aef6a 33671:4b0f2599ed48
   207       | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form";
   207       | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form";
   208     fun defs [] _ = []
   208     fun defs [] _ = []
   209       | defs (l::[]) r = [one_def l r]
   209       | defs (l::[]) r = [one_def l r]
   210       | defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r);
   210       | defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r);
   211     val fixdefs = defs lhss fixpoint;
   211     val fixdefs = defs lhss fixpoint;
   212     val define_all = fold_map (LocalTheory.define Thm.definitionK);
   212     val define_all = fold_map (Local_Theory.define Thm.definitionK);
   213     val (fixdef_thms : (term * (string * thm)) list, lthy') = lthy
   213     val (fixdef_thms : (term * (string * thm)) list, lthy') = lthy
   214       |> define_all (map (apfst fst) fixes ~~ fixdefs);
   214       |> define_all (map (apfst fst) fixes ~~ fixdefs);
   215     fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2];
   215     fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2];
   216     val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms);
   216     val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms);
   217     val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT);
   217     val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT);
   240         val src = Attrib.internal (K add_unfold);
   240         val src = Attrib.internal (K add_unfold);
   241       in
   241       in
   242         ((thm_name, [src]), [thm])
   242         ((thm_name, [src]), [thm])
   243       end;
   243       end;
   244     val (thmss, lthy'') = lthy'
   244     val (thmss, lthy'') = lthy'
   245       |> fold_map LocalTheory.note (induct_note :: map unfold_note unfold_thms);
   245       |> fold_map Local_Theory.note (induct_note :: map unfold_note unfold_thms);
   246   in
   246   in
   247     (lthy'', names, fixdef_thms, map snd unfold_thms)
   247     (lthy'', names, fixdef_thms, map snd unfold_thms)
   248   end;
   248   end;
   249 
   249 
   250 (*************************************************************************)
   250 (*************************************************************************)
   462       val simps1 : (Attrib.binding * thm list) list =
   462       val simps1 : (Attrib.binding * thm list) list =
   463         map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps);
   463         map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps);
   464       val simps2 : (Attrib.binding * thm list) list =
   464       val simps2 : (Attrib.binding * thm list) list =
   465         map (apsnd (fn thm => [thm])) (flat simps);
   465         map (apsnd (fn thm => [thm])) (flat simps);
   466       val (_, lthy'') = lthy'
   466       val (_, lthy'') = lthy'
   467         |> fold_map LocalTheory.note (simps1 @ simps2);
   467         |> fold_map Local_Theory.note (simps1 @ simps2);
   468     in
   468     in
   469       lthy''
   469       lthy''
   470     end
   470     end
   471     else lthy'
   471     else lthy'
   472   end;
   472   end;