--- 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 \<in> set xs"}
becomes @{prop"x \<in> 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 \<Rightarrow> 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 \<Rightarrow> 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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 *)
--- 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
--- 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
--- 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
--- 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;
+
--- 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 \<Rightarrow> ubasis \<Rightarrow> ubasis set \<Rightarrow> 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 \<noteq> 0"
+lemma node_not_0 [simp]: "node i a S \<noteq> 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]:
- "\<lbrakk>finite A; finite B\<rbrakk>
- \<Longrightarrow> node i x A = node j y B \<longleftrightarrow> i = j \<and> x = y \<and> A = B"
+ "\<lbrakk>finite S; finite T\<rbrakk>
+ \<Longrightarrow> node i a S = node j b T \<longleftrightarrow> i = j \<and> a = b \<and> 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: "\<lbrakk>finite A; y \<in> A\<rbrakk> \<Longrightarrow> y < node i x A"
+lemma node_gt2: "\<lbrakk>finite S; b \<in> S\<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> P"
- assumes 2: "\<And>i y A. \<lbrakk>finite A; x = node i y A\<rbrakk> \<Longrightarrow> P"
+ assumes 2: "\<And>i a S. \<lbrakk>finite S; x = node i a S\<rbrakk> \<Longrightarrow> P"
shows "P"
apply (cases x)
apply (erule 1)
@@ -65,7 +65,7 @@
lemma node_induct:
assumes 1: "P 0"
- assumes 2: "\<And>i x A. \<lbrakk>P x; finite A; \<forall>y\<in>A. P y\<rbrakk> \<Longrightarrow> P (node i x A)"
+ assumes 2: "\<And>i a S. \<lbrakk>P a; finite S; \<forall>b\<in>S. P b\<rbrakk> \<Longrightarrow> 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 \<Rightarrow> nat \<Rightarrow> bool"
where
- ubasis_le_refl: "ubasis_le x x"
+ ubasis_le_refl: "ubasis_le a a"
| ubasis_le_trans:
- "\<lbrakk>ubasis_le x y; ubasis_le y z\<rbrakk> \<Longrightarrow> ubasis_le x z"
+ "\<lbrakk>ubasis_le a b; ubasis_le b c\<rbrakk> \<Longrightarrow> ubasis_le a c"
| ubasis_le_lower:
- "finite A \<Longrightarrow> ubasis_le x (node i x A)"
+ "finite S \<Longrightarrow> ubasis_le a (node i a S)"
| ubasis_le_upper:
- "\<lbrakk>finite A; y \<in> A; ubasis_le x y\<rbrakk> \<Longrightarrow> ubasis_le (node i x A) y"
+ "\<lbrakk>finite S; b \<in> S; ubasis_le a b\<rbrakk> \<Longrightarrow> 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 \<Rightarrow> bool) \<Rightarrow> ubasis \<Rightarrow> ubasis"
where
"ubasis_until P 0 = 0"
-| "finite A \<Longrightarrow> 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 \<Longrightarrow> 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 "\<And>i x A y. \<lbrakk>finite A; P (node i x A); y \<in> A; ubasis_le x y\<rbrakk> \<Longrightarrow> P y"
- shows "ubasis_le x y \<Longrightarrow> ubasis_le (ubasis_until P x) (ubasis_until P y)"
+ assumes "\<And>i a S b. \<lbrakk>finite S; P (node i a S); b \<in> S; ubasis_le a b\<rbrakk> \<Longrightarrow> P b"
+ shows "ubasis_le a b \<Longrightarrow> 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 \<le> n \<longleftrightarrow> 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 \<longleftrightarrow> x = compact_bot"
+using rank_le_iff [of x 0] by auto
+
definition
rank_le :: "'a compact_basis \<Rightarrow> 'a compact_basis set"
where
@@ -558,15 +564,15 @@
lemma rank_lt_Un_rank_eq: "rank_lt x \<union> 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 \<Rightarrow> nat"
+ place :: "'a compact_basis \<Rightarrow> 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) \<le> reorder x"
-unfolding reorder_def by simp
+lemma place_ge: "card (rank_lt x) \<le> 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 \<Longrightarrow> reorder x < reorder y"
-apply (rule less_le_trans [OF reorder_bounded])
-apply (rule order_trans [OF _ reorder_ge])
+ shows "rank x < rank y \<Longrightarrow> 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 \<Longrightarrow> x = y"
+lemma place_eqD: "place x = place y \<Longrightarrow> 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 \<Rightarrow> 'a compact_basis"
+where
+ "sub x = (case rank x of 0 \<Rightarrow> compact_bot | Suc k \<Rightarrow> cb_take k x)"
+
+lemma rank_sub_less: "x \<noteq> compact_bot \<Longrightarrow> 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 \<noteq> compact_bot \<Longrightarrow> place (sub x) < place x"
+apply (rule place_rank_mono)
+apply (erule rank_sub_less)
+done
+
+lemma sub_below: "sub x \<sqsubseteq> x"
+unfolding sub_def by (cases "rank x", simp_all add: cb_take_less)
+
+lemma rank_less_imp_below_sub: "\<lbrakk>x \<sqsubseteq> y; rank x < rank y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> sub y"
+unfolding sub_def
+apply (cases "rank y", simp)
+apply (simp add: less_Suc_eq_le)
+apply (subgoal_tac "cb_take nat x \<sqsubseteq> cb_take nat y")
+apply (simp add: rank_leD)
+apply (erule cb_take_mono)
+done
+
function
basis_emb :: "'a compact_basis \<Rightarrow> ubasis"
where
"basis_emb x = (if x = compact_bot then 0 else
- node
- (reorder x)
- (case rank x of 0 \<Rightarrow> 0 | Suc k \<Rightarrow> basis_emb (cb_take k x))
- (basis_emb ` {y. reorder y < reorder x \<and> x \<sqsubseteq> y}))"
+ node (place x) (basis_emb (sub x))
+ (basis_emb ` {y. place y < place x \<and> x \<sqsubseteq> 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 \<and> x \<sqsubseteq> y}"
+lemma fin1: "finite {y. place y < place x \<and> x \<sqsubseteq> 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 \<and> x \<sqsubseteq> y})"
+lemma fin2: "finite (basis_emb ` {y. place y < place x \<and> x \<sqsubseteq> y})"
by (rule finite_imageI [OF fin1])
-lemma basis_emb_mono [OF refl]:
- "\<lbrakk>n = max (reorder x) (reorder y); x \<sqsubseteq> y\<rbrakk>
- \<Longrightarrow> ubasis_le (basis_emb x) (basis_emb y)"
-proof (induct n arbitrary: x y rule: less_induct)
+lemma rank_place_mono:
+ "\<lbrakk>place x < place y; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> 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 \<sqsubseteq> y \<Longrightarrow> ubasis_le (basis_emb x) (basis_emb y)"
+proof (induct n \<equiv> "max (place x) (place y)" arbitrary: x y rule: less_induct)
case (less n)
- assume IH:
- "\<And>(m::nat) (x::'a compact_basis) y.
- \<lbrakk>m < n; m = max (reorder x) (reorder y); x \<sqsubseteq> y\<rbrakk>
- \<Longrightarrow> ubasis_le (basis_emb x) (basis_emb y)"
- assume n: "n = max (reorder x) (reorder y)"
- assume less: "x \<sqsubseteq> y"
- show ?case
- proof (cases)
- assume "x = compact_bot"
- thus ?case by (simp add: ubasis_le_minimal)
- next
- assume x_neq [simp]: "x \<noteq> compact_bot"
- with less have y_neq [simp]: "y \<noteq> compact_bot"
- apply clarify
- apply (drule antisym_less [OF compact_bot_minimal])
- apply simp
+ hence IH:
+ "\<And>(a::'a compact_basis) b.
+ \<lbrakk>max (place a) (place b) < max (place x) (place y); a \<sqsubseteq> b\<rbrakk>
+ \<Longrightarrow> 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 \<sqsubseteq> 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 \<sqsubseteq> 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 \<sqsubseteq> 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 \<sqsubseteq> 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 \<Rightarrow> 'a compact_basis"
+ basis_prj :: "ubasis \<Rightarrow> 'a compact_basis"
where
"basis_prj x = inv basis_emb
- (ubasis_until (\<lambda>x. x \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)) x)"
+ (ubasis_until (\<lambda>x. x \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> ubasis)) x)"
lemma basis_prj_basis_emb: "\<And>x. basis_prj (basis_emb x) = x"
unfolding basis_prj_def
@@ -758,8 +755,8 @@
done
lemma basis_prj_node:
- "\<lbrakk>finite A; node i x A \<notin> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)\<rbrakk>
- \<Longrightarrow> basis_prj (node i x A) = (basis_prj x :: 'a compact_basis)"
+ "\<lbrakk>finite S; node i a S \<notin> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)\<rbrakk>
+ \<Longrightarrow> 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 \<Longrightarrow> basis_prj x \<sqsubseteq> basis_prj y"
- apply (erule ubasis_le.induct)
- apply (rule refl_less)
- apply (erule (1) trans_less)
- apply (case_tac "node i x A \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> 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 \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> 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 \<Longrightarrow> node i a S = basis_emb x \<longleftrightarrow>
+ x \<noteq> compact_bot \<and> i = place x \<and> a = basis_emb (sub x) \<and>
+ S = basis_emb ` {y. place y < place x \<and> x \<sqsubseteq> 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 \<Longrightarrow> basis_prj a \<sqsubseteq> 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 \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> 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 \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> 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} *}