first version of partial_function package

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Partial_Function.thy	Sat Oct 23 23:41:19 2010 +0200
@@ -0,0 +1,247 @@
+(* Title:    HOL/Partial_Function.thy
+   Author:   Alexander Krauss, TU Muenchen
+*)
+
+header {* Partial Function Definitions *}
+
+theory Partial_Function
+imports Complete_Partial_Order Option
+uses 
+  "Tools/Function/function_lib.ML" 
+  "Tools/Function/partial_function.ML" 
+begin
+
+setup Partial_Function.setup
+
+subsection {* Axiomatic setup *}
+
+text {* This techical locale constains the requirements for function
+  definitions with ccpo fixed points.  *}
+
+definition "fun_ord ord f g \<longleftrightarrow> (\<forall>x. ord (f x) (g x))"
+definition "fun_lub L A = (\<lambda>x. L {y. \<exists>f\<in>A. y = f x})"
+definition "img_ord f ord = (\<lambda>x y. ord (f x) (f y))"
+definition "img_lub f g Lub = (\<lambda>A. g (Lub (f ` A)))"
+
+lemma call_mono[partial_function_mono]: "monotone (fun_ord ord) ord (\<lambda>f. f t)"
+by (rule monotoneI) (auto simp: fun_ord_def)
+
+lemma if_mono[partial_function_mono]: "monotone orda ordb F 
+\<Longrightarrow> monotone orda ordb G
+\<Longrightarrow> monotone orda ordb (\<lambda>f. if c then F f else G f)"
+unfolding monotone_def by simp
+
+definition "mk_less R = (\<lambda>x y. R x y \<and> \<not> R y x)"
+
+locale partial_function_definitions = 
+  fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  fixes lub :: "'a set \<Rightarrow> 'a"
+  assumes leq_refl: "leq x x"
+  assumes leq_trans: "leq x y \<Longrightarrow> leq y z \<Longrightarrow> leq x z"
+  assumes leq_antisym: "leq x y \<Longrightarrow> leq y x \<Longrightarrow> x = y"
+  assumes lub_upper: "chain leq A \<Longrightarrow> x \<in> A \<Longrightarrow> leq x (lub A)"
+  assumes lub_least: "chain leq A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> leq x z) \<Longrightarrow> leq (lub A) z"
+
+lemma partial_function_lift:
+  assumes "partial_function_definitions ord lb"
+  shows "partial_function_definitions (fun_ord ord) (fun_lub lb)" (is "partial_function_definitions ?ordf ?lubf")
+proof -
+  interpret partial_function_definitions ord lb by fact
+
+  { fix A a assume A: "chain ?ordf A"
+    have "chain ord {y. \<exists>f\<in>A. y = f a}" (is "chain ord ?C")
+    proof (rule chainI)
+      fix x y assume "x \<in> ?C" "y \<in> ?C"
+      then obtain f g where fg: "f \<in> A" "g \<in> A" 
+        and [simp]: "x = f a" "y = g a" by blast
+      from chainD[OF A fg]
+      show "ord x y \<or> ord y x" unfolding fun_ord_def by auto
+    qed }
+  note chain_fun = this
+
+  show ?thesis
+  proof
+    fix x show "?ordf x x"
+      unfolding fun_ord_def by (auto simp: leq_refl)
+  next
+    fix x y z assume "?ordf x y" "?ordf y z"
+    thus "?ordf x z" unfolding fun_ord_def 
+      by (force dest: leq_trans)
+  next
+    fix x y assume "?ordf x y" "?ordf y x"
+    thus "x = y" unfolding fun_ord_def
+      by (force intro!: ext dest: leq_antisym)
+  next
+    fix A f assume f: "f \<in> A" and A: "chain ?ordf A"
+    thus "?ordf f (?lubf A)"
+      unfolding fun_lub_def fun_ord_def
+      by (blast intro: lub_upper chain_fun[OF A] f)
+  next
+    fix A :: "('b \<Rightarrow> 'a) set" and g :: "'b \<Rightarrow> 'a"
+    assume A: "chain ?ordf A" and g: "\<And>f. f \<in> A \<Longrightarrow> ?ordf f g"
+    show "?ordf (?lubf A) g" unfolding fun_lub_def fun_ord_def
+      by (blast intro: lub_least chain_fun[OF A] dest: g[unfolded fun_ord_def])
+   qed
+qed
+
+lemma ccpo: assumes "partial_function_definitions ord lb"
+  shows "class.ccpo ord (mk_less ord) lb"
+using assms unfolding partial_function_definitions_def mk_less_def
+by unfold_locales blast+
+
+lemma partial_function_image:
+  assumes "partial_function_definitions ord Lub"
+  assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y"
+  assumes inv: "\<And>x. f (g x) = x"
+  shows "partial_function_definitions (img_ord f ord) (img_lub f g Lub)"
+proof -
+  let ?iord = "img_ord f ord"
+  let ?ilub = "img_lub f g Lub"
+
+  interpret partial_function_definitions ord Lub by fact
+  show ?thesis
+  proof
+    fix A x assume "chain ?iord A" "x \<in> A"
+    then have "chain ord (f ` A)" "f x \<in> f ` A"
+      by (auto simp: img_ord_def intro: chainI dest: chainD)
+    thus "?iord x (?ilub A)"
+      unfolding inv img_lub_def img_ord_def by (rule lub_upper)
+  next
+    fix A x assume "chain ?iord A"
+      and 1: "\<And>z. z \<in> A \<Longrightarrow> ?iord z x"
+    then have "chain ord (f ` A)"
+      by (auto simp: img_ord_def intro: chainI dest: chainD)
+    thus "?iord (?ilub A) x"
+      unfolding inv img_lub_def img_ord_def
+      by (rule lub_least) (auto dest: 1[unfolded img_ord_def])
+  qed (auto simp: img_ord_def intro: leq_refl dest: leq_trans leq_antisym inj)
+qed
+
+context partial_function_definitions
+begin
+
+abbreviation "le_fun \<equiv> fun_ord leq"
+abbreviation "lub_fun \<equiv> fun_lub lub"
+abbreviation "fixp_fun == ccpo.fixp le_fun lub_fun"
+abbreviation "mono_body \<equiv> monotone le_fun leq"
+
+text {* Interpret manually, to avoid flooding everything with facts about
+  orders *}
+
+lemma ccpo: "class.ccpo le_fun (mk_less le_fun) lub_fun"
+apply (rule ccpo)
+apply (rule partial_function_lift)
+apply (rule partial_function_definitions_axioms)
+done
+
+text {* The crucial fixed-point theorem *}
+
+lemma mono_body_fixp: 
+  "(\<And>x. mono_body (\<lambda>f. F f x)) \<Longrightarrow> fixp_fun F = F (fixp_fun F)"
+by (rule ccpo.fixp_unfold[OF ccpo]) (auto simp: monotone_def fun_ord_def)
+
+text {* Version with curry/uncurry combinators, to be used by package *}
+
+lemma fixp_rule_uc:
+  fixes F :: "'c \<Rightarrow> 'c" and
+    U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and
+    C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c"
+  assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)"
+  assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
+  assumes inverse: "\<And>f. C (U f) = f"
+  shows "f = F f"
+proof -
+  have "f = C (fixp_fun (\<lambda>f. U (F (C f))))" by (simp add: eq)
+  also have "... = C (U (F (C (fixp_fun (\<lambda>f. U (F (C f)))))))"
+    by (subst mono_body_fixp[of "%f. U (F (C f))", OF mono]) (rule refl)
+  also have "... = F (C (fixp_fun (\<lambda>f. U (F (C f)))))" by (rule inverse)
+  also have "... = F f" by (simp add: eq)
+  finally show "f = F f" .
+qed
+
+text {* Rules for @{term mono_body}: *}
+
+lemma const_mono[partial_function_mono]: "monotone ord leq (\<lambda>f. c)"
+by (rule monotoneI) (rule leq_refl)
+
+declaration {* Partial_Function.init @{term fixp_fun}
+  @{term mono_body} @{thm fixp_rule_uc} *}
+
+end
+
+
+subsection {* Flat interpretation: tailrec and option *}
+
+definition 
+  "flat_ord b x y \<longleftrightarrow> x = b \<or> x = y"
+
+definition 
+  "flat_lub b A = (if A \<subseteq> {b} then b else (THE x. x \<in> A - {b}))"
+
+lemma flat_interpretation:
+  "partial_function_definitions (flat_ord b) (flat_lub b)"
+proof
+  fix A x assume 1: "chain (flat_ord b) A" "x \<in> A"
+  show "flat_ord b x (flat_lub b A)"
+  proof cases
+    assume "x = b"
+    thus ?thesis by (simp add: flat_ord_def)
+  next
+    assume "x \<noteq> b"
+    with 1 have "A - {b} = {x}"
+      by (auto elim: chainE simp: flat_ord_def)
+    then have "flat_lub b A = x"
+      by (auto simp: flat_lub_def)
+    thus ?thesis by (auto simp: flat_ord_def)
+  qed
+next
+  fix A z assume A: "chain (flat_ord b) A"
+    and z: "\<And>x. x \<in> A \<Longrightarrow> flat_ord b x z"
+  show "flat_ord b (flat_lub b A) z"
+  proof cases
+    assume "A \<subseteq> {b}"
+    thus ?thesis
+      by (auto simp: flat_lub_def flat_ord_def)
+  next
+    assume nb: "\<not> A \<subseteq> {b}"
+    then obtain y where y: "y \<in> A" "y \<noteq> b" by auto
+    with A have "A - {b} = {y}"
+      by (auto elim: chainE simp: flat_ord_def)
+    with nb have "flat_lub b A = y"
+      by (auto simp: flat_lub_def)
+    with z y show ?thesis by auto    
+  qed
+qed (auto simp: flat_ord_def)
+
+interpretation tailrec!:
+  partial_function_definitions "flat_ord undefined" "flat_lub undefined"
+by (rule flat_interpretation)
+
+interpretation option!:
+  partial_function_definitions "flat_ord None" "flat_lub None"
+by (rule flat_interpretation)
+
+abbreviation "option_ord \<equiv> flat_ord None"
+abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord"
+
+lemma bind_mono[partial_function_mono]:
+assumes mf: "mono_option B" and mg: "\<And>y. mono_option (\<lambda>f. C y f)"
+shows "mono_option (\<lambda>f. Option.bind (B f) (\<lambda>y. C y f))"
+proof (rule monotoneI)
+  fix f g :: "'a \<Rightarrow> 'b option" assume fg: "fun_ord option_ord f g"
+  with mf
+  have "option_ord (B f) (B g)" by (rule monotoneD[of _ _ _ f g])
+  then have "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y. C y f))"
+    unfolding flat_ord_def by auto    
+  also from mg
+  have "\<And>y'. option_ord (C y' f) (C y' g)"
+    by (rule monotoneD) (rule fg)
+  then have "option_ord (Option.bind (B g) (\<lambda>y'. C y' f)) (Option.bind (B g) (\<lambda>y'. C y' g))"
+    unfolding flat_ord_def by (cases "B g") auto
+  finally (option.leq_trans)
+  show "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y'. C y' g))" .
+qed
+
+
+end
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Function/partial_function.ML	Sat Oct 23 23:41:19 2010 +0200
@@ -0,0 +1,238 @@
+(*  Title:      HOL/Tools/Function/partial_function.ML
+    Author:     Alexander Krauss, TU Muenchen
+
+Partial function definitions based on least fixed points in ccpos.
+*)
+
+signature PARTIAL_FUNCTION =
+sig
+  val setup: theory -> theory
+  val init: term -> term -> thm -> declaration
+
+  val add_partial_function: string -> (binding * typ option * mixfix) list ->
+    Attrib.binding * term -> local_theory -> local_theory
+
+  val add_partial_function_cmd: string -> (binding * string option * mixfix) list ->
+    Attrib.binding * string -> local_theory -> local_theory
+end;
+
+
+structure Partial_Function: PARTIAL_FUNCTION =
+struct
+
+(*** Context Data ***)
+
+structure Modes = Generic_Data
+(
+  type T = ((term * term) * thm) Symtab.table;
+  val empty = Symtab.empty;
+  val extend = I;
+  fun merge (a, b) = Symtab.merge (K true) (a, b);
+)
+
+fun init fixp mono fixp_eq phi =
+  let
+    val term = Morphism.term phi;
+    val data' = ((term fixp, term mono), Morphism.thm phi fixp_eq);
+    val mode = (* extract mode identifier from morphism prefix! *)
+      Binding.prefix_of (Morphism.binding phi (Binding.empty))
+      |> map fst |> space_implode ".";
+  in
+    if mode = "" then I
+    else Modes.map (Symtab.update (mode, data'))
+  end
+
+val known_modes = Symtab.keys o Modes.get o Context.Proof;
+val lookup_mode = Symtab.lookup o Modes.get o Context.Proof;
+
+
+structure Mono_Rules = Named_Thms
+(
+  val name = "partial_function_mono";
+  val description = "monotonicity rules for partial function definitions";
+);
+
+
+(*** Automated monotonicity proofs ***)
+
+fun strip_cases ctac = ctac #> Seq.map snd;
+
+(*rewrite conclusion with k-th assumtion*)
+fun rewrite_with_asm_tac ctxt k =
+  Subgoal.FOCUS (fn {context=ctxt', prems, ...} =>
+    Local_Defs.unfold_tac ctxt' [nth prems k]) ctxt;
+
+fun dest_case thy t =
+  case strip_comb t of
+    (Const (case_comb, _), args) =>
+      (case Datatype.info_of_case thy case_comb of
+         NONE => NONE
+       | SOME {case_rewrites, ...} =>
+           let
+             val lhs = prop_of (hd case_rewrites)
+               |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst;
+             val arity = length (snd (strip_comb lhs));
+             val conv = funpow (length args - arity) Conv.fun_conv
+               (Conv.rewrs_conv (map mk_meta_eq case_rewrites));
+           in
+             SOME (nth args (arity - 1), conv)
+           end)
+  | _ => NONE;
+
+(*split on case expressions*)
+val split_cases_tac = Subgoal.FOCUS_PARAMS (fn {context=ctxt, ...} =>
+  SUBGOAL (fn (t, i) => case t of
+    _ $ (_ $ Abs (_, _, body)) =>
+      (case dest_case (ProofContext.theory_of ctxt) body of
+         NONE => no_tac
+       | SOME (arg, conv) =>
+           let open Conv in
+              if not (null (loose_bnos arg)) then no_tac
+              else ((DETERM o strip_cases o Induct.cases_tac ctxt false [[SOME arg]] NONE [])
+                THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0)
+                THEN_ALL_NEW etac @{thm thin_rl}
+                THEN_ALL_NEW (CONVERSION
+                  (params_conv ~1 (fn ctxt' =>
+                    arg_conv (arg_conv (abs_conv (K conv) ctxt'))) ctxt))) i
+           end)
+  | _ => no_tac) 1);
+
+(*monotonicity proof: apply rules + split case expressions*)
+fun mono_tac ctxt =
+  K (Local_Defs.unfold_tac ctxt [@{thm curry_def}])
+  THEN' (TRY o REPEAT_ALL_NEW
+   (resolve_tac (Mono_Rules.get ctxt)
+     ORELSE' split_cases_tac ctxt));
+
+
+(*** Auxiliary functions ***)
+
+(*positional instantiation with computed type substitution.
+  internal version of  attribute "[of s t u]".*)
+fun cterm_instantiate' cts thm =
+  let
+    val thy = Thm.theory_of_thm thm;
+    val vs = rev (Term.add_vars (prop_of thm) [])
+      |> map (Thm.cterm_of thy o Var);
+  in
+    cterm_instantiate (zip_options vs cts) thm
+  end;
+
+(*Returns t $ u, but instantiates the type of t to make the
+application type correct*)
+fun apply_inst ctxt t u =
+  let
+    val thy = ProofContext.theory_of ctxt;
+    val T = domain_type (fastype_of t);
+    val T' = fastype_of u;
+    val subst = Type.typ_match (Sign.tsig_of thy) (T, T') Vartab.empty
+      handle Type.TYPE_MATCH => raise TYPE ("apply_inst", [T, T'], [t, u])
+  in
+    map_types (Envir.norm_type subst) t $ u
+  end;
+
+fun head_conv cv ct =
+  if can Thm.dest_comb ct then Conv.fun_conv (head_conv cv) ct else cv ct;
+
+
+(*** currying transformation ***)
+
+fun curry_const (A, B, C) =
+  Const (@{const_name Product_Type.curry},
+    [HOLogic.mk_prodT (A, B) --> C, A, B] ---> C);
+
+fun mk_curry f =
+  case fastype_of f of
+    Type ("fun", [Type (_, [S, T]), U]) =>
+      curry_const (S, T, U) $ f
+  | T => raise TYPE ("mk_curry", [T], [f]);
+
+(* iterated versions. Nonstandard left-nested tuples arise naturally
+from "split o split o split"*)
+fun curry_n arity = funpow (arity - 1) mk_curry;
+fun uncurry_n arity = funpow (arity - 1) HOLogic.mk_split;
+
+val curry_uncurry_ss = HOL_basic_ss addsimps
+  [@{thm Product_Type.curry_split}, @{thm Product_Type.split_curry}]
+
+
+(*** partial_function definition ***)
+
+fun gen_add_partial_function prep mode fixes_raw eqn_raw lthy =
+  let
+    val ((fixp, mono), fixp_eq) = the (lookup_mode lthy mode)
+      handle Option.Option => error (cat_lines ["Unknown mode " ^ quote mode ^ ".",
+        "Known modes are " ^ commas_quote (known_modes lthy) ^ "."]);
+
+    val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [eqn_raw] lthy;
+    val (_, _, plain_eqn) = Function_Lib.dest_all_all_ctx lthy eqn;
+
+    val ((f_binding, fT), mixfix) = the_single fixes;
+    val fname = Binding.name_of f_binding;
+
+    val cert = cterm_of (ProofContext.theory_of lthy);
+    val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop plain_eqn);
+    val (head, args) = strip_comb lhs;
+    val F = fold_rev lambda (head :: args) rhs;
+
+    val arity = length args;
+    val (aTs, bTs) = chop arity (binder_types fT);
+
+    val tupleT = foldl1 HOLogic.mk_prodT aTs;
+    val fT_uc = tupleT :: bTs ---> body_type fT;
+    val f_uc = Var ((fname, 0), fT_uc);
+    val x_uc = Var (("x", 0), tupleT);
+    val uncurry = lambda head (uncurry_n arity head);
+    val curry = lambda f_uc (curry_n arity f_uc);
+
+    val F_uc =
+      lambda f_uc (uncurry_n arity (F $ curry_n arity f_uc));
+
+    val mono_goal = apply_inst lthy mono (lambda f_uc (F_uc $ f_uc $ x_uc))
+      |> HOLogic.mk_Trueprop
+      |> Logic.all x_uc;
+
+    val mono_thm = Goal.prove_internal [] (cert mono_goal)
+        (K (mono_tac lthy 1))
+      |> Thm.forall_elim (cert x_uc);
+
+    val f_def_rhs = curry_n arity (apply_inst lthy fixp F_uc);
+    val f_def_binding = Binding.conceal (Binding.name (Thm.def_name fname));
+    val ((f, (_, f_def)), lthy') = Local_Theory.define
+      ((f_binding, mixfix), ((f_def_binding, []), f_def_rhs)) lthy;
+
+    val eqn = HOLogic.mk_eq (list_comb (f, args),
+        Term.betapplys (F, f :: args))
+      |> HOLogic.mk_Trueprop;
+
+    val unfold =
+      (cterm_instantiate' (map (SOME o cert) [uncurry, F, curry]) fixp_eq
+        OF [mono_thm, f_def])
+      |> Tactic.rule_by_tactic lthy (Simplifier.simp_tac curry_uncurry_ss 1);
+
+    val rec_rule = let open Conv in
+      Goal.prove lthy' (map (fst o dest_Free) args) [] eqn (fn _ =>
+        CONVERSION ((arg_conv o arg1_conv o head_conv o rewr_conv) (mk_meta_eq unfold)) 1
+        THEN rtac @{thm refl} 1) end;
+  in
+    lthy'
+    |> Local_Theory.note (eq_abinding, [rec_rule])
+    |-> (fn (_, rec') =>
+      Local_Theory.note ((Binding.qualify true fname (Binding.name "rec"), []), rec'))
+    |> snd
+  end;
+
+val add_partial_function = gen_add_partial_function Specification.check_spec;
+val add_partial_function_cmd = gen_add_partial_function Specification.read_spec;
+
+val mode = Parse.$$$ "(" |-- Parse.xname --| Parse.$$$ ")";
+
+val _ = Outer_Syntax.local_theory
+  "partial_function" "define partial function" Keyword.thy_goal
+  ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
+     >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
+
+
+val setup = Mono_Rules.setup;
+
+end