# HG changeset patch # User wenzelm # Date 1269296455 -3600 # Node ID 4008220110886e467917067ea5d462f5a1a9b88f # Parent 3d699b736ff4ca63e29718f5e8d22708e97368f9# Parent a4ed7aaa7d035b34007d285f73612dd241388a5c merged diff -r a4ed7aaa7d03 -r 400822011088 src/HOLCF/Tools/Domain/domain_library.ML --- 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; diff -r a4ed7aaa7d03 -r 400822011088 src/HOLCF/Tools/fixrec.ML --- 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 diff -r a4ed7aaa7d03 -r 400822011088 src/HOLCF/Tools/pcpodef.ML --- 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 diff -r a4ed7aaa7d03 -r 400822011088 src/HOLCF/Tools/repdef.ML --- 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));