--- a/src/HOLCF/Tools/Domain/domain_library.ML Mon Mar 22 22:56:46 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_library.ML Mon Mar 22 23:20:55 2010 +0100
@@ -212,6 +212,7 @@
fun con_app2 con f args = list_ccomb(%%:con,map f args);
fun con_app con = con_app2 con %#;
fun prj _ _ x ( _::[]) _ = x
+ | prj _ _ _ [] _ = error "Domain_Library.prj: empty list"
| prj f1 _ x (_::y::ys) 0 = f1 x y
| prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1);
fun proj x = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
--- a/src/HOLCF/Tools/fixrec.ML Mon Mar 22 22:56:46 2010 +0100
+++ b/src/HOLCF/Tools/fixrec.ML Mon Mar 22 23:20:55 2010 +0100
@@ -275,12 +275,16 @@
(* this is the pattern-matching compiler function *)
fun compile_pats match_name eqs =
let
- val (((n::names),(a::arities)),mats) =
+ val ((names, arities), mats) =
apfst ListPair.unzip (ListPair.unzip (map (match_eq match_name) eqs));
- val cname = if forall (fn x => n=x) names then n
- else fixrec_err "all equations in block must define the same function";
- val arity = if forall (fn x => a=x) arities then a
- else fixrec_err "all equations in block must have the same arity";
+ val cname =
+ case distinct (op =) names of
+ [n] => n
+ | _ => fixrec_err "all equations in block must define the same function";
+ val arity =
+ case distinct (op =) arities of
+ [a] => a
+ | _ => fixrec_err "all equations in block must have the same arity";
val rhs = fatbar arity mats;
in
mk_trp (cname === rhs)
@@ -311,7 +315,8 @@
else HOLogic.dest_Trueprop (Logic.strip_imp_concl t);
fun tac (t, i) =
let
- val Const (c, T) = head_of (chead_of (fst (HOLogic.dest_eq (concl t))));
+ val (c, T) =
+ (dest_Const o head_of o chead_of o fst o HOLogic.dest_eq o concl) t;
val unfold_thm = the (Symtab.lookup tab c);
val rule = unfold_thm RS @{thm ssubst_lhs};
in
--- a/src/HOLCF/Tools/pcpodef.ML Mon Mar 22 22:56:46 2010 +0100
+++ b/src/HOLCF/Tools/pcpodef.ML Mon Mar 22 23:20:55 2010 +0100
@@ -87,29 +87,32 @@
val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible'];
val (full_tname, Ts) = dest_Type newT;
val lhs_sorts = map (snd o dest_TFree) Ts;
- val thy2 =
- thy
- |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
- (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
+ val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1;
+ val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) tac thy;
(* transfer thms so that they will know about the new cpo instance *)
- val cpo_thms' = map (Thm.transfer thy2) cpo_thms;
+ val cpo_thms' = map (Thm.transfer thy) cpo_thms;
fun make thm = Drule.export_without_context (thm OF cpo_thms');
- val ([adm, cont_Rep, cont_Abs, lub, thelub, compact], thy3) =
- thy2
+ val cont_Rep = make @{thm typedef_cont_Rep};
+ val cont_Abs = make @{thm typedef_cont_Abs};
+ val lub = make @{thm typedef_lub};
+ val thelub = make @{thm typedef_thelub};
+ val compact = make @{thm typedef_compact};
+ val (_, thy) =
+ thy
|> Sign.add_path (Binding.name_of name)
|> PureThy.add_thms
- ([((Binding.prefix_name "adm_" name, admissible'), []),
- ((Binding.prefix_name "cont_" Rep_name, make @{thm typedef_cont_Rep}), []),
- ((Binding.prefix_name "cont_" Abs_name, make @{thm typedef_cont_Abs}), []),
- ((Binding.prefix_name "lub_" name, make @{thm typedef_lub}), []),
- ((Binding.prefix_name "thelub_" name, make @{thm typedef_thelub}), []),
- ((Binding.prefix_name "compact_" name, make @{thm typedef_compact}), [])])
- ||> Sign.restore_naming thy2;
+ ([((Binding.prefix_name "adm_" name, admissible'), []),
+ ((Binding.prefix_name "cont_" Rep_name, cont_Rep ), []),
+ ((Binding.prefix_name "cont_" Abs_name, cont_Abs ), []),
+ ((Binding.prefix_name "lub_" name, lub ), []),
+ ((Binding.prefix_name "thelub_" name, thelub ), []),
+ ((Binding.prefix_name "compact_" name, compact ), [])])
+ ||> Sign.parent_path;
val cpo_info : cpo_info =
{ below_def = below_def, adm = admissible', cont_Rep = cont_Rep,
cont_Abs = cont_Abs, lub = lub, thelub = thelub, compact = compact };
in
- (cpo_info, thy3)
+ (cpo_info, thy)
end;
fun prove_pcpo
@@ -127,29 +130,33 @@
val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, UU_mem'];
val (full_tname, Ts) = dest_Type newT;
val lhs_sorts = map (snd o dest_TFree) Ts;
- val thy2 = thy
- |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
- (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
- val pcpo_thms' = map (Thm.transfer thy2) pcpo_thms;
+ val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1;
+ val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) tac thy;
+ val pcpo_thms' = map (Thm.transfer thy) pcpo_thms;
fun make thm = Drule.export_without_context (thm OF pcpo_thms');
- val ([Rep_strict, Abs_strict, Rep_strict_iff, Abs_strict_iff,
- Rep_defined, Abs_defined], thy3) =
- thy2
+ val Rep_strict = make @{thm typedef_Rep_strict};
+ val Abs_strict = make @{thm typedef_Abs_strict};
+ val Rep_strict_iff = make @{thm typedef_Rep_strict_iff};
+ val Abs_strict_iff = make @{thm typedef_Abs_strict_iff};
+ val Rep_defined = make @{thm typedef_Rep_defined};
+ val Abs_defined = make @{thm typedef_Abs_defined};
+ val (_, thy) =
+ thy
|> Sign.add_path (Binding.name_of name)
|> PureThy.add_thms
- ([((Binding.suffix_name "_strict" Rep_name, make @{thm typedef_Rep_strict}), []),
- ((Binding.suffix_name "_strict" Abs_name, make @{thm typedef_Abs_strict}), []),
- ((Binding.suffix_name "_strict_iff" Rep_name, make @{thm typedef_Rep_strict_iff}), []),
- ((Binding.suffix_name "_strict_iff" Abs_name, make @{thm typedef_Abs_strict_iff}), []),
- ((Binding.suffix_name "_defined" Rep_name, make @{thm typedef_Rep_defined}), []),
- ((Binding.suffix_name "_defined" Abs_name, make @{thm typedef_Abs_defined}), [])])
- ||> Sign.restore_naming thy2;
+ ([((Binding.suffix_name "_strict" Rep_name, Rep_strict), []),
+ ((Binding.suffix_name "_strict" Abs_name, Abs_strict), []),
+ ((Binding.suffix_name "_strict_iff" Rep_name, Rep_strict_iff), []),
+ ((Binding.suffix_name "_strict_iff" Abs_name, Abs_strict_iff), []),
+ ((Binding.suffix_name "_defined" Rep_name, Rep_defined), []),
+ ((Binding.suffix_name "_defined" Abs_name, Abs_defined), [])])
+ ||> Sign.parent_path;
val pcpo_info =
{ Rep_strict = Rep_strict, Abs_strict = Abs_strict,
Rep_strict_iff = Rep_strict_iff, Abs_strict_iff = Abs_strict_iff,
Rep_defined = Rep_defined, Abs_defined = Abs_defined };
in
- (pcpo_info, thy3)
+ (pcpo_info, thy)
end;
(* prepare_cpodef *)
@@ -319,7 +326,8 @@
val args = map (apsnd (prep_constraint ctxt)) raw_args;
val (goal1, goal2, make_result) =
prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
- fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2);
+ fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
+ | after_qed _ = error "cpodef_proof";
in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
fun gen_pcpodef_proof prep_term prep_constraint
@@ -329,7 +337,8 @@
val args = map (apsnd (prep_constraint ctxt)) raw_args;
val (goal1, goal2, make_result) =
prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
- fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2);
+ fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
+ | after_qed _ = error "pcpodef_proof";
in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
in
--- a/src/HOLCF/Tools/repdef.ML Mon Mar 22 22:56:46 2010 +0100
+++ b/src/HOLCF/Tools/repdef.ML Mon Mar 22 23:20:55 2010 +0100
@@ -68,14 +68,14 @@
thy |> Theory.copy |> Theory_Target.init NONE
|> Typedecl.predeclare_constraints (tname, raw_args, mx);
val defl = prep_term tmp_lthy raw_defl;
- val tmp_lthy' = tmp_lthy |> Variable.declare_constraints defl;
+ val tmp_lthy = tmp_lthy |> Variable.declare_constraints defl;
val deflT = Term.fastype_of defl;
val _ = if deflT = @{typ "udom alg_defl"} then ()
else error ("Not type udom alg_defl: " ^ quote (Syntax.string_of_typ tmp_lthy deflT));
(*lhs*)
- val lhs_tfrees = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy' (a, ~1))) raw_args;
+ val lhs_tfrees = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy (a, ~1))) raw_args;
val lhs_sorts = map snd lhs_tfrees;
val full_tname = Sign.full_name thy tname;
val newT = Type (full_tname, map TFree lhs_tfrees);
@@ -91,7 +91,7 @@
(*pcpodef*)
val tac1 = rtac @{thm CollectI} 1 THEN rtac @{thm bottom_in_deflation} 1;
val tac2 = rtac @{thm adm_mem_Collect_in_deflation} 1;
- val ((info, cpo_info, pcpo_info), thy2) = thy
+ val ((info, cpo_info, pcpo_info), thy) = thy
|> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2);
(*definitions*)
@@ -105,44 +105,49 @@
--> alg_deflT udomT --> natT --> (newT ->> newT));
val approx_eqn = Logic.mk_equals (approx_const newT,
repdef_approx_const $ Rep_const $ Abs_const $ defl);
+ val name_def = Binding.suffix_name "_def" name;
+ val emb_bind = (Binding.prefix_name "emb_" name_def, []);
+ val prj_bind = (Binding.prefix_name "prj_" name_def, []);
+ val approx_bind = (Binding.prefix_name "approx_" name_def, []);
(*instantiate class rep*)
- val name_def = Binding.suffix_name "_def" name;
- val ([emb_ldef, prj_ldef, approx_ldef], lthy3) = thy2
- |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort rep})
- |> fold_map Specification.definition
- [ (NONE, ((Binding.prefix_name "emb_" name_def, []), emb_eqn))
- , (NONE, ((Binding.prefix_name "prj_" name_def, []), prj_eqn))
- , (NONE, ((Binding.prefix_name "approx_" name_def, []), approx_eqn)) ]
- |>> map (snd o snd);
- val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy3);
- val [emb_def, prj_def, approx_def] =
- ProofContext.export lthy3 ctxt_thy [emb_ldef, prj_ldef, approx_ldef];
+ val lthy = thy
+ |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort rep});
+ val ((_, (_, emb_ldef)), lthy) =
+ Specification.definition (NONE, (emb_bind, emb_eqn)) lthy;
+ val ((_, (_, prj_ldef)), lthy) =
+ Specification.definition (NONE, (prj_bind, prj_eqn)) lthy;
+ val ((_, (_, approx_ldef)), lthy) =
+ Specification.definition (NONE, (approx_bind, approx_eqn)) lthy;
+ val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
+ val emb_def = singleton (ProofContext.export lthy ctxt_thy) emb_ldef;
+ val prj_def = singleton (ProofContext.export lthy ctxt_thy) prj_ldef;
+ val approx_def = singleton (ProofContext.export lthy ctxt_thy) approx_ldef;
val type_definition_thm =
MetaSimplifier.rewrite_rule
(the_list (#set_def info))
(#type_definition info);
val typedef_thms =
[type_definition_thm, #below_def cpo_info, emb_def, prj_def, approx_def];
- val thy4 = lthy3
+ val thy = lthy
|> Class.prove_instantiation_instance
(K (Tactic.rtac (@{thm typedef_rep_class} OF typedef_thms) 1))
|> Local_Theory.exit_global;
(*other theorems*)
- val typedef_thms' = map (Thm.transfer thy4)
+ val typedef_thms' = map (Thm.transfer thy)
[type_definition_thm, #below_def cpo_info, emb_def, prj_def];
- val ([REP_thm], thy5) = thy4
+ val (REP_thm, thy) = thy
|> Sign.add_path (Binding.name_of name)
- |> PureThy.add_thms
- [((Binding.prefix_name "REP_" name,
- Drule.export_without_context (@{thm typedef_REP} OF typedef_thms')), [])]
- ||> Sign.restore_naming thy4;
+ |> PureThy.add_thm
+ ((Binding.prefix_name "REP_" name,
+ Drule.export_without_context (@{thm typedef_REP} OF typedef_thms')), [])
+ ||> Sign.restore_naming thy;
val rep_info =
{ emb_def = emb_def, prj_def = prj_def, approx_def = approx_def, REP = REP_thm };
in
- ((info, cpo_info, pcpo_info, rep_info), thy5)
+ ((info, cpo_info, pcpo_info, rep_info), thy)
end
handle ERROR msg =>
cat_error msg ("The error(s) above occurred in repdef " ^ quote (Binding.str_of name));