# HG changeset patch # User haftmann # Date 1236968287 -3600 # Node ID c4728771f04f26537449ad24bcdea4ab4f21a3ac # Parent 68b4a06cbd5c03ac1f64fdb3c68cc41052f12e51# Parent c05c0199826f157c7e843e91b44e2f55a92b3858 merged diff -r c05c0199826f -r c4728771f04f doc-src/LaTeXsugar/Sugar/Sugar.thy --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Fri Mar 13 19:17:58 2009 +0100 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Fri Mar 13 19:18:07 2009 +0100 @@ -92,7 +92,7 @@ the $n$th element of @{text xs}. \item Human readers are good at converting automatically from lists to -sets. Hence \texttt{OptionalSugar} contains syntax for supressing the +sets. Hence \texttt{OptionalSugar} contains syntax for suppressing the conversion function @{const set}: for example, @{prop[source]"x \ set xs"} becomes @{prop"x \ set xs"}. @@ -106,6 +106,17 @@ \end{itemize} *} +subsection{* Numbers *} + +text{* Coercions between numeric types are alien to mathematicians who +consider, for example, @{typ nat} as a subset of @{typ int}. +\texttt{OptionalSugar} contains syntax for suppressing numeric coercions such +as @{const int} @{text"::"} @{typ"nat \ int"}. For example, +@{term[source]"int 5"} is printed as @{term "int 5"}. Embeddings of types +@{typ nat}, @{typ int}, @{typ real} are covered; non-injective coercions such +as @{const nat} @{text"::"} @{typ"int \ nat"} are not and should not be +hidden. *} + section "Printing theorems" subsection "Question marks" @@ -126,7 +137,7 @@ at the beginning of your file \texttt{ROOT.ML}. The rest of this document is produced with this flag reset. -Hint: Resetting \verb!show_question_marks! only supresses question +Hint: Resetting \verb!show_question_marks! only suppresses question marks; variables that end in digits, e.g. @{text"x1"}, are still printed with a trailing @{text".0"}, e.g. @{text"x1.0"}, their internal index. This can be avoided by turning the last digit into a diff -r c05c0199826f -r c4728771f04f doc-src/LaTeXsugar/Sugar/document/Sugar.tex --- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Fri Mar 13 19:17:58 2009 +0100 +++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Fri Mar 13 19:18:07 2009 +0100 @@ -120,7 +120,7 @@ the $n$th element of \isa{xs}. \item Human readers are good at converting automatically from lists to -sets. Hence \texttt{OptionalSugar} contains syntax for supressing the +sets. Hence \texttt{OptionalSugar} contains syntax for suppressing the conversion function \isa{set}: for example, \isa{{\isachardoublequote}x\ {\isasymin}\ set\ xs{\isachardoublequote}} becomes \isa{x\ {\isasymin}\ xs}. @@ -137,6 +137,22 @@ \end{isamarkuptext}% \isamarkuptrue% % +\isamarkupsubsection{Numbers% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Coercions between numeric types are alien to mathematicians who +consider, for example, \isa{nat} as a subset of \isa{int}. +\texttt{OptionalSugar} contains syntax for suppressing numeric coercions such +as \isa{int} \isa{{\isacharcolon}{\isacharcolon}} \isa{nat\ {\isasymRightarrow}\ int}. For example, +\isa{{\isachardoublequote}int\ {\isadigit{5}}{\isachardoublequote}} is printed as \isa{{\isadigit{5}}}. Embeddings of types +\isa{nat}, \isa{int}, \isa{real} are covered; non-injective coercions such +as \isa{nat} \isa{{\isacharcolon}{\isacharcolon}} \isa{int\ {\isasymRightarrow}\ nat} are not and should not be +hidden.% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsection{Printing theorems% } \isamarkuptrue% @@ -162,7 +178,7 @@ at the beginning of your file \texttt{ROOT.ML}. The rest of this document is produced with this flag reset. -Hint: Resetting \verb!show_question_marks! only supresses question +Hint: Resetting \verb!show_question_marks! only suppresses question marks; variables that end in digits, e.g. \isa{x{\isadigit{1}}}, are still printed with a trailing \isa{{\isachardot}{\isadigit{0}}}, e.g. \isa{x{\isadigit{1}}{\isachardot}{\isadigit{0}}}, their internal index. This can be avoided by turning the last digit into a diff -r c05c0199826f -r c4728771f04f src/HOL/Library/Numeral_Type.thy --- a/src/HOL/Library/Numeral_Type.thy Fri Mar 13 19:17:58 2009 +0100 +++ b/src/HOL/Library/Numeral_Type.thy Fri Mar 13 19:18:07 2009 +0100 @@ -36,7 +36,7 @@ typed_print_translation {* let - fun card_univ_tr' show_sorts _ [Const (@{const_name UNIV}, Type(_,[T,_]))] = + fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_,[T,_]))] = Syntax.const "_type_card" $ Syntax.term_of_typ show_sorts T; in [(@{const_syntax card}, card_univ_tr')] end diff -r c05c0199826f -r c4728771f04f src/HOL/Library/OptionalSugar.thy --- a/src/HOL/Library/OptionalSugar.thy Fri Mar 13 19:17:58 2009 +0100 +++ b/src/HOL/Library/OptionalSugar.thy Fri Mar 13 19:18:07 2009 +0100 @@ -18,6 +18,8 @@ "n" <= "real n" "n" <= "CONST real_of_nat n" "n" <= "CONST real_of_int n" + "n" <= "CONST of_real n" + "n" <= "CONST complex_of_real n" (* append *) syntax (latex output) @@ -27,6 +29,7 @@ "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)" +(* deprecated, use thm_style instead, will be removed *) (* aligning equations *) notation (tab output) "op =" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and diff -r c05c0199826f -r c4728771f04f src/HOL/Power.thy --- a/src/HOL/Power.thy Fri Mar 13 19:17:58 2009 +0100 +++ b/src/HOL/Power.thy Fri Mar 13 19:18:07 2009 +0100 @@ -412,56 +412,4 @@ by (induct m n rule: diff_induct) (simp_all add: nonzero_mult_divide_cancel_left nz) - -text{*ML bindings for the general exponentiation theorems*} -ML -{* -val power_0 = thm"power_0"; -val power_Suc = thm"power_Suc"; -val power_0_Suc = thm"power_0_Suc"; -val power_0_left = thm"power_0_left"; -val power_one = thm"power_one"; -val power_one_right = thm"power_one_right"; -val power_add = thm"power_add"; -val power_mult = thm"power_mult"; -val power_mult_distrib = thm"power_mult_distrib"; -val zero_less_power = thm"zero_less_power"; -val zero_le_power = thm"zero_le_power"; -val one_le_power = thm"one_le_power"; -val gt1_imp_ge0 = thm"gt1_imp_ge0"; -val power_gt1_lemma = thm"power_gt1_lemma"; -val power_gt1 = thm"power_gt1"; -val power_le_imp_le_exp = thm"power_le_imp_le_exp"; -val power_inject_exp = thm"power_inject_exp"; -val power_less_imp_less_exp = thm"power_less_imp_less_exp"; -val power_mono = thm"power_mono"; -val power_strict_mono = thm"power_strict_mono"; -val power_eq_0_iff = thm"power_eq_0_iff"; -val field_power_eq_0_iff = thm"power_eq_0_iff"; -val field_power_not_zero = thm"field_power_not_zero"; -val power_inverse = thm"power_inverse"; -val nonzero_power_divide = thm"nonzero_power_divide"; -val power_divide = thm"power_divide"; -val power_abs = thm"power_abs"; -val zero_less_power_abs_iff = thm"zero_less_power_abs_iff"; -val zero_le_power_abs = thm "zero_le_power_abs"; -val power_minus = thm"power_minus"; -val power_Suc_less = thm"power_Suc_less"; -val power_strict_decreasing = thm"power_strict_decreasing"; -val power_decreasing = thm"power_decreasing"; -val power_Suc_less_one = thm"power_Suc_less_one"; -val power_increasing = thm"power_increasing"; -val power_strict_increasing = thm"power_strict_increasing"; -val power_le_imp_le_base = thm"power_le_imp_le_base"; -val power_inject_base = thm"power_inject_base"; -*} - -text{*ML bindings for the remaining theorems*} -ML -{* -val nat_one_le_power = thm"nat_one_le_power"; -val nat_power_less_imp_less = thm"nat_power_less_imp_less"; -val nat_zero_less_power_iff = thm"nat_zero_less_power_iff"; -*} - end diff -r c05c0199826f -r c4728771f04f src/HOL/Tools/function_package/context_tree.ML --- a/src/HOL/Tools/function_package/context_tree.ML Fri Mar 13 19:17:58 2009 +0100 +++ b/src/HOL/Tools/function_package/context_tree.ML Fri Mar 13 19:18:07 2009 +0100 @@ -11,7 +11,7 @@ type ctx_tree (* FIXME: This interface is a mess and needs to be cleaned up! *) - val get_fundef_congs : Context.generic -> thm list + val get_fundef_congs : Proof.context -> thm list val add_fundef_cong : thm -> Context.generic -> Context.generic val map_fundef_congs : (thm list -> thm list) -> Context.generic -> Context.generic @@ -52,8 +52,8 @@ fun merge _ = Thm.merge_thms ); -val map_fundef_congs = FundefCongs.map -val get_fundef_congs = FundefCongs.get +val get_fundef_congs = FundefCongs.get o Context.Proof +val map_fundef_congs = FundefCongs.map val add_fundef_cong = FundefCongs.map o Thm.add_thm (* congruence rules *) @@ -127,7 +127,7 @@ fun mk_tree fvar h ctxt t = let - val congs = get_fundef_congs (Context.Proof ctxt) + val congs = get_fundef_congs ctxt val congs_deps = map (fn c => (c, cong_deps c)) (congs @ default_congs) (* FIXME: Save in theory *) fun matchcall (a $ b) = if a = Free fvar then SOME b else NONE diff -r c05c0199826f -r c4728771f04f src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Fri Mar 13 19:17:58 2009 +0100 +++ b/src/HOL/Tools/function_package/fundef_common.ML Fri Mar 13 19:18:07 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Tools/function_package/fundef_common.ML - ID: $Id$ Author: Alexander Krauss, TU Muenchen A package for general recursive function definitions. @@ -101,6 +100,8 @@ fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2) ); +val get_fundef = FundefData.get o Context.Proof; + (* Generally useful?? *) fun lift_morphism thy f = @@ -113,7 +114,7 @@ fun import_fundef_data t ctxt = let - val thy = Context.theory_of ctxt + val thy = ProofContext.theory_of ctxt val ct = cterm_of thy t val inst_morph = lift_morphism thy o Thm.instantiate @@ -121,20 +122,20 @@ SOME (morph_fundef_data data (inst_morph (Thm.match (cterm_of thy trm, ct)))) handle Pattern.MATCH => NONE in - get_first match (NetRules.retrieve (FundefData.get ctxt) t) + get_first match (NetRules.retrieve (get_fundef ctxt) t) end fun import_last_fundef ctxt = - case NetRules.rules (FundefData.get ctxt) of + case NetRules.rules (get_fundef ctxt) of [] => NONE | (t, data) :: _ => let - val ([t'], ctxt') = Variable.import_terms true [t] (Context.proof_of ctxt) + val ([t'], ctxt') = Variable.import_terms true [t] ctxt in - import_fundef_data t' (Context.Proof ctxt') + import_fundef_data t' ctxt' end -val all_fundef_data = NetRules.rules o FundefData.get +val all_fundef_data = NetRules.rules o get_fundef fun add_fundef_data (data as FundefCtxData {fs, termination, ...}) = FundefData.map (fold (fn f => NetRules.insert (f, data)) fs) @@ -161,7 +162,7 @@ ); val set_termination_prover = TerminationProver.put -val get_termination_prover = TerminationProver.get +val get_termination_prover = TerminationProver.get o Context.Proof (* Configuration management *) diff -r c05c0199826f -r c4728771f04f src/HOL/Tools/function_package/fundef_datatype.ML --- a/src/HOL/Tools/function_package/fundef_datatype.ML Fri Mar 13 19:17:58 2009 +0100 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Fri Mar 13 19:18:07 2009 +0100 @@ -7,11 +7,18 @@ signature FUNDEF_DATATYPE = sig - val pat_complete_tac: Proof.context -> int -> tactic + val pat_completeness_tac: Proof.context -> int -> tactic + val pat_completeness: Proof.context -> Proof.method val prove_completeness : theory -> term list -> term -> term list list -> term list list -> thm - val pat_completeness : Proof.context -> method val setup : theory -> theory + + val add_fun : FundefCommon.fundef_config -> + (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> + bool list -> bool -> local_theory -> Proof.context + val add_fun_cmd : FundefCommon.fundef_config -> + (binding * string option * mixfix) list -> (Attrib.binding * string) list -> + bool list -> bool -> local_theory -> Proof.context end structure FundefDatatype : FUNDEF_DATATYPE = @@ -167,7 +174,7 @@ -fun pat_complete_tac ctxt = SUBGOAL (fn (subgoal, i) => +fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) => let val thy = ProofContext.theory_of ctxt val (vs, subgf) = dest_all_all subgoal @@ -196,15 +203,15 @@ handle COMPLETENESS => no_tac) -fun pat_completeness ctxt = Method.SIMPLE_METHOD' (pat_complete_tac ctxt) +fun pat_completeness ctxt = Method.SIMPLE_METHOD' (pat_completeness_tac ctxt) -val by_pat_completeness_simp = +val by_pat_completeness_auto = Proof.global_future_terminal_proof (Method.Basic (pat_completeness, Position.none), SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none)))) fun termination_by method int = - FundefPackage.setup_termination_proof NONE + FundefPackage.termination_proof NONE #> Proof.global_future_terminal_proof (Method.Basic (method, Position.none), NONE) int @@ -301,24 +308,28 @@ val fun_config = FundefConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), domintros=false, tailrec=false } - -local structure P = OuterParse and K = OuterKeyword in - -fun fun_cmd config fixes statements flags int lthy = +fun gen_fun add config fixes statements flags int lthy = let val group = serial_string () in lthy |> LocalTheory.set_group group - |> FundefPackage.add_fundef fixes statements config flags - |> by_pat_completeness_simp int + |> add fixes statements config flags + |> by_pat_completeness_auto int |> LocalTheory.restore |> LocalTheory.set_group group - |> termination_by (FundefCommon.get_termination_prover (Context.Proof lthy)) int + |> termination_by (FundefCommon.get_termination_prover lthy) int end; +val add_fun = gen_fun FundefPackage.add_fundef +val add_fun_cmd = gen_fun FundefPackage.add_fundef_cmd + + + +local structure P = OuterParse and K = OuterKeyword in + val _ = OuterSyntax.local_theory' "fun" "define general recursive functions (short version)" K.thy_decl (fundef_parser fun_config - >> (fn ((config, fixes), (flags, statements)) => fun_cmd config fixes statements flags)); + >> (fn ((config, fixes), (flags, statements)) => add_fun_cmd config fixes statements flags)); end diff -r c05c0199826f -r c4728771f04f src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Fri Mar 13 19:17:58 2009 +0100 +++ b/src/HOL/Tools/function_package/fundef_package.ML Fri Mar 13 19:18:07 2009 +0100 @@ -7,24 +7,26 @@ signature FUNDEF_PACKAGE = sig - val add_fundef : (binding * string option * mixfix) list + val add_fundef : (binding * typ option * mixfix) list + -> (Attrib.binding * term) list + -> FundefCommon.fundef_config + -> bool list + -> local_theory + -> Proof.state + val add_fundef_cmd : (binding * string option * mixfix) list -> (Attrib.binding * string) list -> FundefCommon.fundef_config -> bool list -> local_theory -> Proof.state - val add_fundef_i: (binding * typ option * mixfix) list - -> (Attrib.binding * term) list - -> FundefCommon.fundef_config - -> bool list - -> local_theory - -> Proof.state - - val setup_termination_proof : string option -> local_theory -> Proof.state + val termination_proof : term option -> local_theory -> Proof.state + val termination_proof_cmd : string option -> local_theory -> Proof.state + val termination : term option -> local_theory -> Proof.state + val termination_cmd : string option -> local_theory -> Proof.state val setup : theory -> theory - val get_congs : theory -> thm list + val get_congs : Proof.context -> thm list end @@ -114,6 +116,10 @@ |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd end +val add_fundef = gen_add_fundef false Specification.check_spec (TypeInfer.anyT HOLogic.typeS) +val add_fundef_cmd = gen_add_fundef true Specification.read_spec "_::type" + + fun total_termination_afterqed data [[totality]] lthy = let val FundefCtxData { add_simps, case_names, psimps, pinducts, defname, ... } = data @@ -136,13 +142,14 @@ |> note_theorem ((qualify "induct", [Attrib.internal (K (RuleCases.case_names case_names))]), tinduct) |> snd end - -fun setup_termination_proof term_opt lthy = +fun gen_termination_proof prep_term raw_term_opt lthy = let + val term_opt = Option.map (prep_term lthy) raw_term_opt val data = the (case term_opt of - SOME t => import_fundef_data (Syntax.read_term lthy t) (Context.Proof lthy) - | NONE => import_last_fundef (Context.Proof lthy)) - handle Option.Option => error ("Not a function: " ^ quote (the_default "" term_opt)) + SOME t => (import_fundef_data t lthy + handle Option.Option => + error ("Not a function: " ^ quote (Syntax.string_of_term lthy t))) + | NONE => (import_last_fundef lthy handle Option.Option => error "Not a function")) val FundefCtxData {termination, R, ...} = data val domT = domain_type (fastype_of R) @@ -157,13 +164,18 @@ |> Proof.theorem_i NONE (total_termination_afterqed data) [[(goal, [])]] end +val termination_proof = gen_termination_proof Syntax.check_term; +val termination_proof_cmd = gen_termination_proof Syntax.read_term; + +fun termination term_opt lthy = + lthy + |> LocalTheory.set_group (serial_string ()) + |> termination_proof term_opt; + fun termination_cmd term_opt lthy = lthy |> LocalTheory.set_group (serial_string ()) - |> setup_termination_proof term_opt; - -val add_fundef = gen_add_fundef true Specification.read_spec "_::type" -val add_fundef_i = gen_add_fundef false Specification.check_spec (TypeInfer.anyT HOLogic.typeS) + |> termination_proof_cmd term_opt; (* Datatype hook to declare datatype congs as "fundef_congs" *) @@ -180,6 +192,7 @@ val setup_case_cong = DatatypePackage.interpretation case_cong + (* setup *) val setup = @@ -190,7 +203,7 @@ #> FundefRelation.setup #> FundefCommon.TerminationSimps.setup -val get_congs = FundefCtxTree.get_fundef_congs o Context.Theory +val get_congs = FundefCtxTree.get_fundef_congs (* outer syntax *) @@ -202,7 +215,7 @@ val _ = OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal (fundef_parser default_config - >> (fn ((config, fixes), (flags, statements)) => add_fundef fixes statements config flags)); + >> (fn ((config, fixes), (flags, statements)) => add_fundef_cmd fixes statements config flags)); val _ = OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal diff -r c05c0199826f -r c4728771f04f src/HOL/Tools/function_package/induction_scheme.ML --- a/src/HOL/Tools/function_package/induction_scheme.ML Fri Mar 13 19:17:58 2009 +0100 +++ b/src/HOL/Tools/function_package/induction_scheme.ML Fri Mar 13 19:18:07 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Tools/function_package/induction_scheme.ML - ID: $Id$ Author: Alexander Krauss, TU Muenchen A method to prove induction schemes. @@ -8,7 +7,8 @@ signature INDUCTION_SCHEME = sig val mk_ind_tac : (int -> tactic) -> (int -> tactic) -> (int -> tactic) - -> Proof.context -> thm list -> tactic + -> Proof.context -> thm list -> tactic + val induct_scheme_tac : Proof.context -> thm list -> tactic val setup : theory -> theory end @@ -395,8 +395,11 @@ end)) +fun induct_scheme_tac ctxt = + mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt; + val setup = Method.add_methods - [("induct_scheme", Method.ctxt_args (Method.RAW_METHOD o (fn ctxt => mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt)), + [("induct_scheme", Method.ctxt_args (Method.RAW_METHOD o induct_scheme_tac), "proves an induction principle")] end diff -r c05c0199826f -r c4728771f04f src/HOL/Tools/function_package/lexicographic_order.ML --- a/src/HOL/Tools/function_package/lexicographic_order.ML Fri Mar 13 19:17:58 2009 +0100 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML Fri Mar 13 19:18:07 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Tools/function_package/lexicographic_order.ML - ID: $Id$ Author: Lukas Bulwahn, TU Muenchen Method for termination proofs with lexicographic orderings. @@ -7,8 +6,9 @@ signature LEXICOGRAPHIC_ORDER = sig - val lexicographic_order : thm list -> Proof.context -> Method.method - val lexicographic_order_tac : Proof.context -> tactic -> tactic + val lex_order_tac : Proof.context -> tactic -> tactic + val lexicographic_order_tac : Proof.context -> tactic + val lexicographic_order : Proof.context -> Proof.method val setup: theory -> theory end @@ -186,9 +186,10 @@ end (** The Main Function **) -fun lexicographic_order_tac ctxt solve_tac (st: thm) = + +fun lex_order_tac ctxt solve_tac (st: thm) = let - val thy = theory_of_thm st + val thy = ProofContext.theory_of ctxt val ((trueprop $ (wf $ rel)) :: tl) = prems_of st val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel)) @@ -213,12 +214,15 @@ THEN EVERY (map prove_row clean_table)) end -fun lexicographic_order thms ctxt = - Method.SIMPLE_METHOD (TRY (FundefCommon.apply_termination_rule ctxt 1) - THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.TerminationSimps.get ctxt))) +fun lexicographic_order_tac ctxt = + TRY (FundefCommon.apply_termination_rule ctxt 1) + THEN lex_order_tac ctxt (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.TerminationSimps.get ctxt)) + +val lexicographic_order = Method.SIMPLE_METHOD o lexicographic_order_tac -val setup = Method.add_methods [("lexicographic_order", Method.bang_sectioned_args clasimp_modifiers lexicographic_order, +val setup = Method.add_methods [("lexicographic_order", Method.only_sectioned_args clasimp_modifiers lexicographic_order, "termination prover for lexicographic orderings")] - #> Context.theory_map (FundefCommon.set_termination_prover (lexicographic_order [])) + #> Context.theory_map (FundefCommon.set_termination_prover lexicographic_order) -end +end; + diff -r c05c0199826f -r c4728771f04f src/HOLCF/Universal.thy --- a/src/HOLCF/Universal.thy Fri Mar 13 19:17:58 2009 +0100 +++ b/src/HOLCF/Universal.thy Fri Mar 13 19:18:07 2009 +0100 @@ -13,35 +13,35 @@ definition node :: "nat \ ubasis \ ubasis set \ ubasis" where - "node i x A = Suc (prod2nat (i, prod2nat (x, set2nat A)))" + "node i a S = Suc (prod2nat (i, prod2nat (a, set2nat S)))" -lemma node_not_0 [simp]: "node i x A \ 0" +lemma node_not_0 [simp]: "node i a S \ 0" unfolding node_def by simp -lemma node_gt_0 [simp]: "0 < node i x A" +lemma node_gt_0 [simp]: "0 < node i a S" unfolding node_def by simp lemma node_inject [simp]: - "\finite A; finite B\ - \ node i x A = node j y B \ i = j \ x = y \ A = B" + "\finite S; finite T\ + \ node i a S = node j b T \ i = j \ a = b \ S = T" unfolding node_def by simp -lemma node_gt0: "i < node i x A" +lemma node_gt0: "i < node i a S" unfolding node_def less_Suc_eq_le by (rule le_prod2nat_1) -lemma node_gt1: "x < node i x A" +lemma node_gt1: "a < node i a S" unfolding node_def less_Suc_eq_le by (rule order_trans [OF le_prod2nat_1 le_prod2nat_2]) lemma nat_less_power2: "n < 2^n" by (induct n) simp_all -lemma node_gt2: "\finite A; y \ A\ \ y < node i x A" +lemma node_gt2: "\finite S; b \ S\ \ b < node i a S" unfolding node_def less_Suc_eq_le set2nat_def apply (rule order_trans [OF _ le_prod2nat_2]) apply (rule order_trans [OF _ le_prod2nat_2]) -apply (rule order_trans [where y="setsum (op ^ 2) {y}"]) +apply (rule order_trans [where y="setsum (op ^ 2) {b}"]) apply (simp add: nat_less_power2 [THEN order_less_imp_le]) apply (erule setsum_mono2, simp, simp) done @@ -52,7 +52,7 @@ lemma node_cases: assumes 1: "x = 0 \ P" - assumes 2: "\i y A. \finite A; x = node i y A\ \ P" + assumes 2: "\i a S. \finite S; x = node i a S\ \ P" shows "P" apply (cases x) apply (erule 1) @@ -65,7 +65,7 @@ lemma node_induct: assumes 1: "P 0" - assumes 2: "\i x A. \P x; finite A; \y\A. P y\ \ P (node i x A)" + assumes 2: "\i a S. \P a; finite S; \b\S. P b\ \ P (node i a S)" shows "P x" apply (induct x rule: nat_less_induct) apply (case_tac n rule: node_cases) @@ -78,13 +78,13 @@ inductive ubasis_le :: "nat \ nat \ bool" where - ubasis_le_refl: "ubasis_le x x" + ubasis_le_refl: "ubasis_le a a" | ubasis_le_trans: - "\ubasis_le x y; ubasis_le y z\ \ ubasis_le x z" + "\ubasis_le a b; ubasis_le b c\ \ ubasis_le a c" | ubasis_le_lower: - "finite A \ ubasis_le x (node i x A)" + "finite S \ ubasis_le a (node i a S)" | ubasis_le_upper: - "\finite A; y \ A; ubasis_le x y\ \ ubasis_le (node i x A) y" + "\finite S; b \ S; ubasis_le a b\ \ ubasis_le (node i a S) b" lemma ubasis_le_minimal: "ubasis_le 0 x" apply (induct x rule: node_induct) @@ -99,8 +99,8 @@ ubasis_until :: "(ubasis \ bool) \ ubasis \ ubasis" where "ubasis_until P 0 = 0" -| "finite A \ ubasis_until P (node i x A) = - (if P (node i x A) then node i x A else ubasis_until P x)" +| "finite S \ ubasis_until P (node i a S) = + (if P (node i a S) then node i a S else ubasis_until P a)" apply clarify apply (rule_tac x=b in node_cases) apply simp @@ -157,8 +157,8 @@ done lemma ubasis_until_mono: - assumes "\i x A y. \finite A; P (node i x A); y \ A; ubasis_le x y\ \ P y" - shows "ubasis_le x y \ ubasis_le (ubasis_until P x) (ubasis_until P y)" + assumes "\i a S b. \finite S; P (node i a S); b \ S; ubasis_le a b\ \ P b" + shows "ubasis_le a b \ ubasis_le (ubasis_until P a) (ubasis_until P b)" apply (induct set: ubasis_le) apply (rule ubasis_le_refl) apply (erule (1) ubasis_le_trans) @@ -510,6 +510,12 @@ lemma rank_le_iff: "rank x \ n \ cb_take n x = x" by (rule iffI [OF rank_leD rank_leI]) +lemma rank_compact_bot [simp]: "rank compact_bot = 0" +using rank_leI [of 0 compact_bot] by simp + +lemma rank_eq_0_iff [simp]: "rank x = 0 \ x = compact_bot" +using rank_le_iff [of x 0] by auto + definition rank_le :: "'a compact_basis \ 'a compact_basis set" where @@ -558,15 +564,15 @@ lemma rank_lt_Un_rank_eq: "rank_lt x \ rank_eq x = rank_le x" unfolding rank_lt_def rank_eq_def rank_le_def by auto -subsubsection {* Reordering of basis elements *} +subsubsection {* Sequencing basis elements *} definition - reorder :: "'a compact_basis \ nat" + place :: "'a compact_basis \ nat" where - "reorder x = card (rank_lt x) + choose_pos (rank_eq x) x" + "place x = card (rank_lt x) + choose_pos (rank_eq x) x" -lemma reorder_bounded: "reorder x < card (rank_le x)" -unfolding reorder_def +lemma place_bounded: "place x < card (rank_le x)" +unfolding place_def apply (rule ord_less_eq_trans) apply (rule add_strict_left_mono) apply (rule choose_pos_bounded) @@ -579,53 +585,77 @@ apply (simp add: rank_lt_Un_rank_eq) done -lemma reorder_ge: "card (rank_lt x) \ reorder x" -unfolding reorder_def by simp +lemma place_ge: "card (rank_lt x) \ place x" +unfolding place_def by simp -lemma reorder_rank_mono: +lemma place_rank_mono: fixes x y :: "'a compact_basis" - shows "rank x < rank y \ reorder x < reorder y" -apply (rule less_le_trans [OF reorder_bounded]) -apply (rule order_trans [OF _ reorder_ge]) + shows "rank x < rank y \ place x < place y" +apply (rule less_le_trans [OF place_bounded]) +apply (rule order_trans [OF _ place_ge]) apply (rule card_mono) apply (rule finite_rank_lt) apply (simp add: rank_le_def rank_lt_def subset_eq) done -lemma reorder_eqD: "reorder x = reorder y \ x = y" +lemma place_eqD: "place x = place y \ x = y" apply (rule linorder_cases [where x="rank x" and y="rank y"]) - apply (drule reorder_rank_mono, simp) - apply (simp add: reorder_def) + apply (drule place_rank_mono, simp) + apply (simp add: place_def) apply (rule inj_on_choose_pos [where A="rank_eq x", THEN inj_onD]) apply (rule finite_rank_eq) apply (simp cong: rank_lt_cong rank_eq_cong) apply (simp add: rank_eq_def) apply (simp add: rank_eq_def) - apply (drule reorder_rank_mono, simp) + apply (drule place_rank_mono, simp) done -lemma inj_reorder: "inj reorder" -by (rule inj_onI, erule reorder_eqD) +lemma inj_place: "inj place" +by (rule inj_onI, erule place_eqD) subsubsection {* Embedding and projection on basis elements *} +definition + sub :: "'a compact_basis \ 'a compact_basis" +where + "sub x = (case rank x of 0 \ compact_bot | Suc k \ cb_take k x)" + +lemma rank_sub_less: "x \ compact_bot \ rank (sub x) < rank x" +unfolding sub_def +apply (cases "rank x", simp) +apply (simp add: less_Suc_eq_le) +apply (rule rank_leI) +apply (rule cb_take_idem) +done + +lemma place_sub_less: "x \ compact_bot \ place (sub x) < place x" +apply (rule place_rank_mono) +apply (erule rank_sub_less) +done + +lemma sub_below: "sub x \ x" +unfolding sub_def by (cases "rank x", simp_all add: cb_take_less) + +lemma rank_less_imp_below_sub: "\x \ y; rank x < rank y\ \ x \ sub y" +unfolding sub_def +apply (cases "rank y", simp) +apply (simp add: less_Suc_eq_le) +apply (subgoal_tac "cb_take nat x \ cb_take nat y") +apply (simp add: rank_leD) +apply (erule cb_take_mono) +done + function basis_emb :: "'a compact_basis \ ubasis" where "basis_emb x = (if x = compact_bot then 0 else - node - (reorder x) - (case rank x of 0 \ 0 | Suc k \ basis_emb (cb_take k x)) - (basis_emb ` {y. reorder y < reorder x \ x \ y}))" + node (place x) (basis_emb (sub x)) + (basis_emb ` {y. place y < place x \ x \ y}))" by auto termination basis_emb -apply (relation "measure reorder", simp) -apply simp -apply (rule reorder_rank_mono) -apply (simp add: less_Suc_eq_le) -apply (rule rank_leI) -apply (rule cb_take_idem) +apply (relation "measure place", simp) +apply (simp add: place_sub_less) apply simp done @@ -634,101 +664,68 @@ lemma basis_emb_compact_bot [simp]: "basis_emb compact_bot = 0" by (simp add: basis_emb.simps) -lemma fin1: "finite {y. reorder y < reorder x \ x \ y}" +lemma fin1: "finite {y. place y < place x \ x \ y}" apply (subst Collect_conj_eq) apply (rule finite_Int) apply (rule disjI1) -apply (subgoal_tac "finite (reorder -` {n. n < reorder x})", simp) -apply (rule finite_vimageI [OF _ inj_reorder]) +apply (subgoal_tac "finite (place -` {n. n < place x})", simp) +apply (rule finite_vimageI [OF _ inj_place]) apply (simp add: lessThan_def [symmetric]) done -lemma fin2: "finite (basis_emb ` {y. reorder y < reorder x \ x \ y})" +lemma fin2: "finite (basis_emb ` {y. place y < place x \ x \ y})" by (rule finite_imageI [OF fin1]) -lemma basis_emb_mono [OF refl]: - "\n = max (reorder x) (reorder y); x \ y\ - \ ubasis_le (basis_emb x) (basis_emb y)" -proof (induct n arbitrary: x y rule: less_induct) +lemma rank_place_mono: + "\place x < place y; x \ y\ \ rank x < rank y" +apply (rule linorder_cases, assumption) +apply (simp add: place_def cong: rank_lt_cong rank_eq_cong) +apply (drule choose_pos_lessD) +apply (rule finite_rank_eq) +apply (simp add: rank_eq_def) +apply (simp add: rank_eq_def) +apply simp +apply (drule place_rank_mono, simp) +done + +lemma basis_emb_mono: + "x \ y \ ubasis_le (basis_emb x) (basis_emb y)" +proof (induct n \ "max (place x) (place y)" arbitrary: x y rule: less_induct) case (less n) - assume IH: - "\(m::nat) (x::'a compact_basis) y. - \m < n; m = max (reorder x) (reorder y); x \ y\ - \ ubasis_le (basis_emb x) (basis_emb y)" - assume n: "n = max (reorder x) (reorder y)" - assume less: "x \ y" - show ?case - proof (cases) - assume "x = compact_bot" - thus ?case by (simp add: ubasis_le_minimal) - next - assume x_neq [simp]: "x \ compact_bot" - with less have y_neq [simp]: "y \ compact_bot" - apply clarify - apply (drule antisym_less [OF compact_bot_minimal]) - apply simp + hence IH: + "\(a::'a compact_basis) b. + \max (place a) (place b) < max (place x) (place y); a \ b\ + \ ubasis_le (basis_emb a) (basis_emb b)" + by simp + show ?case proof (rule linorder_cases) + assume "place x < place y" + then have "rank x < rank y" + using `x \ y` by (rule rank_place_mono) + with `place x < place y` show ?case + apply (case_tac "y = compact_bot", simp) + apply (simp add: basis_emb.simps [of y]) + apply (rule ubasis_le_trans [OF _ ubasis_le_lower [OF fin2]]) + apply (rule IH) + apply (simp add: less_max_iff_disj) + apply (erule place_sub_less) + apply (erule rank_less_imp_below_sub [OF `x \ y`]) done - show ?case - proof (rule linorder_cases) - assume 1: "reorder x < reorder y" - show ?case - proof (rule linorder_cases) - assume "rank x < rank y" - with 1 show ?case - apply (case_tac "rank y", simp) - apply (subst basis_emb.simps [where x=y]) - apply simp - apply (rule ubasis_le_trans [OF _ ubasis_le_lower [OF fin2]]) - apply (rule IH [OF _ refl, unfolded n]) - apply (simp add: less_max_iff_disj) - apply (rule reorder_rank_mono) - apply (simp add: less_Suc_eq_le) - apply (rule rank_leI) - apply (rule cb_take_idem) - apply (simp add: less_Suc_eq_le) - apply (subgoal_tac "cb_take nat x \ cb_take nat y") - apply (simp add: rank_leD) - apply (rule cb_take_mono [OF less]) - done - next - assume "rank x = rank y" - with 1 show ?case - apply (simp add: reorder_def) - apply (simp cong: rank_lt_cong rank_eq_cong) - apply (drule choose_pos_lessD) - apply (rule finite_rank_eq) - apply (simp add: rank_eq_def) - apply (simp add: rank_eq_def) - apply (simp add: less) - done - next - assume "rank x > rank y" - hence "reorder x > reorder y" - by (rule reorder_rank_mono) - with 1 show ?case by simp - qed - next - assume "reorder x = reorder y" - hence "x = y" by (rule reorder_eqD) - thus ?case by (simp add: ubasis_le_refl) - next - assume "reorder x > reorder y" - with less show ?case - apply (simp add: basis_emb.simps [where x=x]) - apply (rule ubasis_le_upper [OF fin2], simp) - apply (cases "rank x") - apply (simp add: ubasis_le_minimal) - apply simp - apply (rule IH [OF _ refl, unfolded n]) - apply (simp add: less_max_iff_disj) - apply (rule reorder_rank_mono) - apply (simp add: less_Suc_eq_le) - apply (rule rank_leI) - apply (rule cb_take_idem) - apply (erule rev_trans_less) - apply (rule cb_take_less) - done - qed + next + assume "place x = place y" + hence "x = y" by (rule place_eqD) + thus ?case by (simp add: ubasis_le_refl) + next + assume "place x > place y" + with `x \ y` show ?case + apply (case_tac "x = compact_bot", simp add: ubasis_le_minimal) + apply (simp add: basis_emb.simps [of x]) + apply (rule ubasis_le_upper [OF fin2], simp) + apply (rule IH) + apply (simp add: less_max_iff_disj) + apply (erule place_sub_less) + apply (erule rev_trans_less) + apply (rule sub_below) + done qed qed @@ -740,14 +737,14 @@ apply (simp add: basis_emb.simps) apply (simp add: basis_emb.simps) apply (simp add: basis_emb.simps) - apply (simp add: fin2 inj_eq [OF inj_reorder]) + apply (simp add: fin2 inj_eq [OF inj_place]) done definition - basis_prj :: "nat \ 'a compact_basis" + basis_prj :: "ubasis \ 'a compact_basis" where "basis_prj x = inv basis_emb - (ubasis_until (\x. x \ range (basis_emb :: 'a compact_basis \ nat)) x)" + (ubasis_until (\x. x \ range (basis_emb :: 'a compact_basis \ ubasis)) x)" lemma basis_prj_basis_emb: "\x. basis_prj (basis_emb x) = x" unfolding basis_prj_def @@ -758,8 +755,8 @@ done lemma basis_prj_node: - "\finite A; node i x A \ range (basis_emb :: 'a compact_basis \ nat)\ - \ basis_prj (node i x A) = (basis_prj x :: 'a compact_basis)" + "\finite S; node i a S \ range (basis_emb :: 'a compact_basis \ nat)\ + \ basis_prj (node i a S) = (basis_prj a :: 'a compact_basis)" unfolding basis_prj_def by simp lemma basis_prj_0: "basis_prj 0 = compact_bot" @@ -767,32 +764,41 @@ apply (rule basis_prj_basis_emb) done -lemma basis_prj_mono: "ubasis_le x y \ basis_prj x \ basis_prj y" - apply (erule ubasis_le.induct) - apply (rule refl_less) - apply (erule (1) trans_less) - apply (case_tac "node i x A \ range (basis_emb :: 'a compact_basis \ nat)") - apply (erule rangeE, rename_tac a) - apply (case_tac "a = compact_bot", simp) - apply (simp add: basis_prj_basis_emb) - apply (simp add: basis_emb.simps) - apply (clarsimp simp add: fin2) - apply (case_tac "rank a", simp) - apply (simp add: basis_prj_0) - apply (simp add: basis_prj_basis_emb) - apply (rule cb_take_less) - apply (simp add: basis_prj_node) - apply (case_tac "node i x A \ range (basis_emb :: 'a compact_basis \ nat)") - apply (erule rangeE, rename_tac a) - apply (case_tac "a = compact_bot", simp) - apply (simp add: basis_prj_basis_emb) - apply (simp add: basis_emb.simps) - apply (clarsimp simp add: fin2) - apply (case_tac "rank a", simp add: basis_prj_basis_emb) - apply (simp add: basis_prj_basis_emb) - apply (simp add: basis_prj_node) +lemma node_eq_basis_emb_iff: + "finite S \ node i a S = basis_emb x \ + x \ compact_bot \ i = place x \ a = basis_emb (sub x) \ + S = basis_emb ` {y. place y < place x \ x \ y}" +apply (cases "x = compact_bot", simp) +apply (simp add: basis_emb.simps [of x]) +apply (simp add: fin2) done +lemma basis_prj_mono: "ubasis_le a b \ basis_prj a \ basis_prj b" +proof (induct a b rule: ubasis_le.induct) + case (ubasis_le_refl a) show ?case by (rule refl_less) +next + case (ubasis_le_trans a b c) thus ?case by - (rule trans_less) +next + case (ubasis_le_lower S a i) thus ?case + apply (case_tac "node i a S \ range (basis_emb :: 'a compact_basis \ nat)") + apply (erule rangeE, rename_tac x) + apply (simp add: basis_prj_basis_emb) + apply (simp add: node_eq_basis_emb_iff) + apply (simp add: basis_prj_basis_emb) + apply (rule sub_below) + apply (simp add: basis_prj_node) + done +next + case (ubasis_le_upper S b a i) thus ?case + apply (case_tac "node i a S \ range (basis_emb :: 'a compact_basis \ nat)") + apply (erule rangeE, rename_tac x) + apply (simp add: basis_prj_basis_emb) + apply (clarsimp simp add: node_eq_basis_emb_iff) + apply (simp add: basis_prj_basis_emb) + apply (simp add: basis_prj_node) + done +qed + lemma basis_emb_prj_less: "ubasis_le (basis_emb (basis_prj x)) x" unfolding basis_prj_def apply (subst f_inv_f [where f=basis_emb]) @@ -806,7 +812,8 @@ node choose choose_pos - reorder + place + sub subsubsection {* EP-pair from any bifinite domain into @{typ udom} *}