Switched function package to use the new package for inductive predicates.
authorkrauss
Wed Oct 18 16:13:03 2006 +0200 (2006-10-18)
changeset 21051c49467a9c1e1
parent 21050 d0447a511edb
child 21052 ec5531061ed6
Switched function package to use the new package for inductive predicates.
src/HOL/FunDef.thy
src/HOL/Tools/function_package/context_tree.ML
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_datatype.ML
src/HOL/Tools/function_package/fundef_lib.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/fundef_prep.ML
src/HOL/Tools/function_package/fundef_proof.ML
src/HOL/Tools/function_package/inductive_wrap.ML
src/HOL/Tools/function_package/mutual.ML
src/HOL/Tools/function_package/pattern_split.ML
src/HOL/Tools/function_package/termination.ML
src/HOL/ex/Fundefs.thy
     1.1 --- a/src/HOL/FunDef.thy	Wed Oct 18 10:15:39 2006 +0200
     1.2 +++ b/src/HOL/FunDef.thy	Wed Oct 18 16:13:03 2006 +0200
     1.3 @@ -23,6 +23,89 @@
     1.4  ("Tools/function_package/auto_term.ML")
     1.5  begin
     1.6  
     1.7 +section {* Wellfoundedness and Accessibility: Predicate versions *}
     1.8 +
     1.9 +
    1.10 +constdefs
    1.11 +  wfP         :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
    1.12 +  "wfP(r) == (!P. (!x. (!y. r y x --> P(y)) --> P(x)) --> (!x. P(x)))"
    1.13 +
    1.14 +lemma wfP_induct: 
    1.15 +    "[| wfP r;           
    1.16 +        !!x.[| ALL y. r y x --> P(y) |] ==> P(x)  
    1.17 +     |]  ==>  P(a)"
    1.18 +by (unfold wfP_def, blast)
    1.19 +
    1.20 +lemmas wfP_induct_rule = wfP_induct [rule_format, consumes 1, case_names less]
    1.21 +
    1.22 +definition in_rel_def[simp]:
    1.23 +  "in_rel R x y == (x, y) \<in> R"
    1.24 +
    1.25 +lemma wf_in_rel:
    1.26 +  "wf R \<Longrightarrow> wfP (in_rel R)"
    1.27 +  unfolding wfP_def wf_def in_rel_def .
    1.28 +
    1.29 +
    1.30 +inductive2 accP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
    1.31 +  for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.32 +intros
    1.33 +    accPI: "(!!y. r y x ==> accP r y) ==> accP r x"
    1.34 +
    1.35 +
    1.36 +theorem accP_induct:
    1.37 +  assumes major: "accP r a"
    1.38 +  assumes hyp: "!!x. accP r x ==> \<forall>y. r y x --> P y ==> P x"
    1.39 +  shows "P a"
    1.40 +  apply (rule major [THEN accP.induct])
    1.41 +  apply (rule hyp)
    1.42 +   apply (rule accPI)
    1.43 +   apply fast
    1.44 +  apply fast
    1.45 +  done
    1.46 +
    1.47 +theorems accP_induct_rule = accP_induct [rule_format, induct set: accP]
    1.48 +
    1.49 +theorem accP_downward: "accP r b ==> r a b ==> accP r a"
    1.50 +  apply (erule accP.cases)
    1.51 +  apply fast
    1.52 +  done
    1.53 +
    1.54 +
    1.55 +lemma accP_subset:
    1.56 +  assumes sub: "\<And>x y. R1 x y \<Longrightarrow> R2 x y"
    1.57 +  shows "\<And>x. accP R2 x \<Longrightarrow> accP R1 x"
    1.58 +proof-
    1.59 +  fix x assume "accP R2 x"
    1.60 +  then show "accP R1 x"
    1.61 +  proof (induct x)
    1.62 +    fix x
    1.63 +    assume ih: "\<And>y. R2 y x \<Longrightarrow> accP R1 y"
    1.64 +    with sub show "accP R1 x"
    1.65 +      by (blast intro:accPI)
    1.66 +  qed
    1.67 +qed
    1.68 +
    1.69 +
    1.70 +lemma accP_subset_induct:
    1.71 +  assumes subset: "\<And>x. D x \<Longrightarrow> accP R x"
    1.72 +    and dcl: "\<And>x z. \<lbrakk>D x; R z x\<rbrakk> \<Longrightarrow> D z"
    1.73 +    and "D x"
    1.74 +    and istep: "\<And>x. \<lbrakk>D x; (\<And>z. R z x \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x"
    1.75 +  shows "P x"
    1.76 +proof -
    1.77 +  from subset and `D x` 
    1.78 +  have "accP R x" .
    1.79 +  then show "P x" using `D x`
    1.80 +  proof (induct x)
    1.81 +    fix x
    1.82 +    assume "D x"
    1.83 +      and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y"
    1.84 +    with dcl and istep show "P x" by blast
    1.85 +  qed
    1.86 +qed
    1.87 +
    1.88 +
    1.89 +section {* Definitions with default value *}
    1.90  
    1.91  definition
    1.92    THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a"
    1.93 @@ -41,37 +124,41 @@
    1.94  
    1.95  
    1.96  lemma fundef_ex1_existence:
    1.97 -assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)"
    1.98 -assumes ex1: "\<exists>!y. (x,y)\<in>G"
    1.99 -shows "(x, f x)\<in>G"
   1.100 +assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
   1.101 +assumes ex1: "\<exists>!y. G x y"
   1.102 +shows "G x (f x)"
   1.103    by (simp only:f_def, rule THE_defaultI', rule ex1)
   1.104  
   1.105 +
   1.106 +
   1.107 +
   1.108 +
   1.109  lemma fundef_ex1_uniqueness:
   1.110 -assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)"
   1.111 -assumes ex1: "\<exists>!y. (x,y)\<in>G"
   1.112 -assumes elm: "(x, h x)\<in>G"
   1.113 +assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
   1.114 +assumes ex1: "\<exists>!y. G x y"
   1.115 +assumes elm: "G x (h x)"
   1.116  shows "h x = f x"
   1.117    by (simp only:f_def, rule THE_default1_equality[symmetric], rule ex1, rule elm)
   1.118  
   1.119  lemma fundef_ex1_iff:
   1.120 -assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)"
   1.121 -assumes ex1: "\<exists>!y. (x,y)\<in>G"
   1.122 -shows "((x, y)\<in>G) = (f x = y)"
   1.123 +assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
   1.124 +assumes ex1: "\<exists>!y. G x y"
   1.125 +shows "(G x y) = (f x = y)"
   1.126    apply (auto simp:ex1 f_def THE_default1_equality)
   1.127    by (rule THE_defaultI', rule ex1)
   1.128  
   1.129  lemma fundef_default_value:
   1.130 -assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)"
   1.131 -assumes graph: "\<And>x y. (x,y) \<in> G \<Longrightarrow> x \<in> D"
   1.132 +assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
   1.133 +assumes graph: "\<And>x y. G x y \<Longrightarrow> x \<in> D"
   1.134  assumes "x \<notin> D"
   1.135  shows "f x = d x"
   1.136  proof -
   1.137 -  have "\<not>(\<exists>y. (x, y) \<in> G)"
   1.138 +  have "\<not>(\<exists>y. G x y)"
   1.139    proof
   1.140 -    assume "(\<exists>y. (x, y) \<in> G)"
   1.141 +    assume "(\<exists>y. G x y)"
   1.142      with graph and `x\<notin>D` show False by blast
   1.143    qed
   1.144 -  hence "\<not>(\<exists>!y. (x, y) \<in> G)" by blast
   1.145 +  hence "\<not>(\<exists>!y. G x y)" by blast
   1.146    
   1.147    thus ?thesis
   1.148      unfolding f_def
   1.149 @@ -80,8 +167,7 @@
   1.150  
   1.151  
   1.152  
   1.153 -
   1.154 -subsection {* Projections *}
   1.155 +section {* Projections *}
   1.156  consts
   1.157    lpg::"(('a + 'b) * 'a) set"
   1.158    rpg::"(('a + 'b) * 'b) set"
   1.159 @@ -105,6 +191,8 @@
   1.160  
   1.161  
   1.162  
   1.163 +lemma P_imp_P: "P \<Longrightarrow> P" .
   1.164 +
   1.165  
   1.166  use "Tools/function_package/sum_tools.ML"
   1.167  use "Tools/function_package/fundef_common.ML"
     2.1 --- a/src/HOL/Tools/function_package/context_tree.ML	Wed Oct 18 10:15:39 2006 +0200
     2.2 +++ b/src/HOL/Tools/function_package/context_tree.ML	Wed Oct 18 16:13:03 2006 +0200
     2.3 @@ -42,6 +42,7 @@
     2.4  struct
     2.5  
     2.6  open FundefCommon
     2.7 +open FundefLib
     2.8  
     2.9  
    2.10  (* Maps "Trueprop A = B" to "A" *)
     3.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Wed Oct 18 10:15:39 2006 +0200
     3.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Wed Oct 18 16:13:03 2006 +0200
     3.3 @@ -10,10 +10,10 @@
     3.4  struct
     3.5  
     3.6  (* Theory Dependencies *)
     3.7 -val acc_const_name = "Accessible_Part.acc"
     3.8 +val acc_const_name = "FunDef.accP"
     3.9  
    3.10  fun mk_acc domT R =
    3.11 -    Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R 
    3.12 +    Const (acc_const_name, (fastype_of R) --> domT --> HOLogic.boolT) $ R 
    3.13  
    3.14  
    3.15  type depgraph = int IntGraph.T
    3.16 @@ -221,36 +221,41 @@
    3.17    = Sequential
    3.18    | Default of string
    3.19    | Preprocessor of string
    3.20 +  | Target of xstring
    3.21  
    3.22  datatype fundef_config
    3.23    = FundefConfig of
    3.24     {
    3.25      sequential: bool,
    3.26      default: string,
    3.27 -    preprocessor: string option
    3.28 +    preprocessor: string option,
    3.29 +    target: xstring option
    3.30     }
    3.31  
    3.32  
    3.33 -val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE }
    3.34 -val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE }
    3.35 +val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE, target=NONE }
    3.36 +val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE, target=NONE }
    3.37  
    3.38 -fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor}) = 
    3.39 -    FundefConfig {sequential=true, default=default, preprocessor=preprocessor }
    3.40 -  | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor}) = 
    3.41 -    FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor }
    3.42 -  | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor}) = 
    3.43 -    FundefConfig {sequential=sequential, default=default, preprocessor=SOME p }
    3.44 +fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target}) = 
    3.45 +    FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target }
    3.46 +  | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target}) = 
    3.47 +    FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target }
    3.48 +  | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target}) = 
    3.49 +    FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target }
    3.50 +  | apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target }) =
    3.51 +    FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t }
    3.52  
    3.53 -    
    3.54 +
    3.55  local structure P = OuterParse and K = OuterKeyword in
    3.56  
    3.57  val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
    3.58  
    3.59  val option_parser = (P.$$$ "sequential" >> K Sequential)
    3.60                 || ((P.reserved "default" |-- P.term) >> Default)
    3.61 +               || ((P.$$$ "in" |-- P.xname) >> Target)
    3.62  
    3.63 -val config_parser = (Scan.optional (P.$$$ "(" |-- P.list1 option_parser --| P.$$$ ")") [])
    3.64 -                      >> (fn opts => fold apply_opt opts default_config)
    3.65 +fun config_parser def = (Scan.optional (P.$$$ "(" |-- P.list1 option_parser --| P.$$$ ")") [])
    3.66 +                          >> (fn opts => fold apply_opt opts def)
    3.67  end
    3.68  
    3.69  
    3.70 @@ -263,6 +268,7 @@
    3.71  
    3.72  
    3.73  
    3.74 +
    3.75  end
    3.76  
    3.77  
     4.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Oct 18 10:15:39 2006 +0200
     4.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Oct 18 16:13:03 2006 +0200
     4.3 @@ -17,6 +17,8 @@
     4.4  structure FundefDatatype : FUNDEF_DATATYPE =
     4.5  struct
     4.6  
     4.7 +open FundefLib
     4.8 +open FundefCommon
     4.9  
    4.10  fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T)
    4.11  fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T)
     5.1 --- a/src/HOL/Tools/function_package/fundef_lib.ML	Wed Oct 18 10:15:39 2006 +0200
     5.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML	Wed Oct 18 16:13:03 2006 +0200
     5.3 @@ -7,6 +7,9 @@
     5.4  *)
     5.5  
     5.6  
     5.7 +
     5.8 +structure FundefLib = struct
     5.9 +
    5.10  fun eq_str (s : string, t) = (s = t) (* monomorphic equality on strings *)
    5.11  
    5.12  fun mk_forall (var as Free (v,T)) t =
    5.13 @@ -128,3 +131,6 @@
    5.14  fun plural sg pl [] = sys_error "plural"
    5.15    | plural sg pl [x] = sg
    5.16    | plural sg pl (x::y::ys) = pl
    5.17 +
    5.18 +
    5.19 +end
    5.20 \ No newline at end of file
     6.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Oct 18 10:15:39 2006 +0200
     6.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Oct 18 16:13:03 2006 +0200
     6.3 @@ -32,6 +32,7 @@
     6.4  structure FundefPackage  =
     6.5  struct
     6.6  
     6.7 +open FundefLib
     6.8  open FundefCommon
     6.9  
    6.10  (*fn (ctxt,s) => Variable.importT_terms (fst (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) [] [s])) ctxt;*)
    6.11 @@ -187,12 +188,13 @@
    6.12  
    6.13  val functionP =
    6.14    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
    6.15 -  ((config_parser -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
    6.16 +  ((config_parser default_config -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
    6.17       >> (fn (((config, target), fixes), statements) =>
    6.18              Toplevel.print o
    6.19              Toplevel.local_theory_to_proof target (add_fundef fixes statements config)));
    6.20  
    6.21  
    6.22 +
    6.23  val terminationP =
    6.24    OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
    6.25    (P.opt_locale_target -- Scan.option P.name
     7.1 --- a/src/HOL/Tools/function_package/fundef_prep.ML	Wed Oct 18 10:15:39 2006 +0200
     7.2 +++ b/src/HOL/Tools/function_package/fundef_prep.ML	Wed Oct 18 16:13:03 2006 +0200
     7.3 @@ -22,13 +22,14 @@
     7.4  struct
     7.5  
     7.6  
     7.7 +open FundefLib
     7.8  open FundefCommon
     7.9  open FundefAbbrev
    7.10  
    7.11  (* Theory dependencies. *)
    7.12  val Pair_inject = thm "Product_Type.Pair_inject";
    7.13  
    7.14 -val acc_induct_rule = thm "Accessible_Part.acc_induct_rule"
    7.15 +val acc_induct_rule = thm "FunDef.accP_induct_rule"
    7.16  
    7.17  val ex1_implies_ex = thm "FunDef.fundef_ex1_existence"
    7.18  val ex1_implies_un = thm "FunDef.fundef_ex1_uniqueness"
    7.19 @@ -143,7 +144,7 @@
    7.20                               |> fold implies_elim_swp rcassm
    7.21  
    7.22                  val h_assum =
    7.23 -                    mk_relmem (rcarg, h $ rcarg) G
    7.24 +                    Trueprop (G $ rcarg $ (h $ rcarg))
    7.25                                |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
    7.26                                |> fold_rev (mk_forall o Free) rcfix
    7.27                                |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
    7.28 @@ -272,20 +273,15 @@
    7.29  
    7.30          val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
    7.31          val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
    7.32 -
    7.33 -        val eq_pairs = assume (cterm_of thy (Trueprop (mk_eq (mk_prod (lhsi, y), mk_prod (lhsj',rhsj'h)))))
    7.34      in
    7.35          (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
    7.36          |> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
    7.37          |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
    7.38          |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
    7.39 +        |> fold_rev (implies_intr o cprop_of) Ghsj'
    7.40 +        |> fold_rev (implies_intr o cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
    7.41          |> implies_intr (cprop_of y_eq_rhsj'h)
    7.42 -        |> implies_intr (cprop_of lhsi_eq_lhsj') (* Gj', Rj1' ... Rjk' |-- [| lhs_i = lhs_j', y = rhs_j_h' |] ==> y = rhs_i_f *)
    7.43 -        |> (fn it => Drule.compose_single(it, 2, Pair_inject)) (* Gj', Rj1' ... Rjk' |-- (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
    7.44 -        |> implies_elim_swp eq_pairs
    7.45 -        |> fold_rev (implies_intr o cprop_of) Ghsj'
    7.46 -        |> fold_rev (implies_intr o cprop_of) agsj' (* Gj', Rj1', ..., Rjk' ==> (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
    7.47 -        |> implies_intr (cprop_of eq_pairs)
    7.48 +        |> implies_intr (cprop_of lhsi_eq_lhsj')
    7.49          |> fold_rev forall_intr (cterm_of thy h :: cqsj')
    7.50      end
    7.51  
    7.52 @@ -305,21 +301,21 @@
    7.53  
    7.54          val existence = fold (curry op COMP o prep_RC) RCs lGI
    7.55  
    7.56 -        val a = cterm_of thy (mk_prod (lhs, y))
    7.57          val P = cterm_of thy (mk_eq (y, rhsC))
    7.58 -        val a_in_G = assume (cterm_of thy (Trueprop (mk_mem (term_of a, G))))
    7.59 +        val G_lhs_y = assume (cterm_of thy (Trueprop (G $ lhs $ y)))
    7.60  
    7.61          val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas
    7.62  
    7.63          val uniqueness = G_cases
    7.64 -                           |> forall_elim a
    7.65 +                           |> forall_elim (cterm_of thy lhs)
    7.66 +                           |> forall_elim (cterm_of thy y)
    7.67                             |> forall_elim P
    7.68 -                           |> implies_elim_swp a_in_G
    7.69 +                           |> implies_elim_swp G_lhs_y
    7.70                             |> fold implies_elim_swp unique_clauses
    7.71 -                           |> implies_intr (cprop_of a_in_G)
    7.72 +                           |> implies_intr (cprop_of G_lhs_y)
    7.73                             |> forall_intr (cterm_of thy y)
    7.74  
    7.75 -        val P2 = cterm_of thy (lambda y (mk_mem (mk_prod (lhs, y), G))) (* P2 y := (lhs, y): G *)
    7.76 +        val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
    7.77  
    7.78          val exactly_one =
    7.79              ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
    7.80 @@ -332,11 +328,11 @@
    7.81  
    7.82          val function_value =
    7.83              existence
    7.84 -                |> implies_intr ihyp
    7.85 -                |> implies_intr (cprop_of case_hyp)
    7.86 -                |> forall_intr (cterm_of thy x)
    7.87 -                |> forall_elim (cterm_of thy lhs)
    7.88 -                |> curry (op RS) refl
    7.89 +              |> implies_intr ihyp
    7.90 +              |> implies_intr (cprop_of case_hyp)
    7.91 +              |> forall_intr (cterm_of thy x)
    7.92 +              |> forall_elim (cterm_of thy lhs)
    7.93 +              |> curry (op RS) refl
    7.94      in
    7.95          (exactly_one, function_value)
    7.96      end
    7.97 @@ -348,15 +344,15 @@
    7.98      let
    7.99          val Globals {h, domT, ranT, x, ...} = globals
   7.100  
   7.101 -        val inst_ex1_ex = f_def RS ex1_implies_ex
   7.102 -        val inst_ex1_un = f_def RS ex1_implies_un
   7.103 +        val inst_ex1_ex =  f_def RS ex1_implies_ex
   7.104 +        val inst_ex1_un =  f_def RS ex1_implies_un
   7.105          val inst_ex1_iff = f_def RS ex1_implies_iff
   7.106  
   7.107          (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
   7.108          val ihyp = all domT $ Abs ("z", domT,
   7.109 -                                   implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R)
   7.110 +                                   implies $ Trueprop (R $ Bound 0 $ x)
   7.111                                             $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
   7.112 -                                                             Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G)))
   7.113 +                                                             Abs ("y", ranT, G $ Bound 1 $ Bound 0)))
   7.114                         |> cterm_of thy
   7.115  
   7.116          val ihyp_thm = assume ihyp |> forall_elim_vars 0
   7.117 @@ -375,7 +371,7 @@
   7.118                                    |> forall_elim_vars 0
   7.119                                    |> fold (curry op COMP) ex1s
   7.120                                    |> implies_intr (ihyp)
   7.121 -                                  |> implies_intr (cterm_of thy (Trueprop (mk_mem (x, mk_acc domT R))))
   7.122 +                                  |> implies_intr (cterm_of thy (Trueprop (mk_acc domT R $ x)))
   7.123                                    |> forall_intr (cterm_of thy x)
   7.124                                    |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
   7.125                                    |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
   7.126 @@ -394,17 +390,17 @@
   7.127  
   7.128  fun define_graph Gname fvar domT ranT clauses RCss lthy =
   7.129      let
   7.130 -      val GT = mk_relT (domT, ranT)
   7.131 +      val GT = domT --> ranT --> boolT
   7.132        val Gvar = Free (the_single (Variable.variant_frees lthy [] [(Gname, GT)]))
   7.133  
   7.134        fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
   7.135            let
   7.136              fun mk_h_assm (rcfix, rcassm, rcarg) =
   7.137 -                mk_relmem (rcarg, fvar $ rcarg) Gvar
   7.138 +                Trueprop (Gvar $ rcarg $ (fvar $ rcarg))
   7.139                            |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
   7.140                            |> fold_rev (mk_forall o Free) rcfix
   7.141            in
   7.142 -            mk_relmem (lhs, rhs) Gvar
   7.143 +            Trueprop (Gvar $ lhs $ rhs)
   7.144                        |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
   7.145                        |> fold_rev (curry Logic.mk_implies) gs
   7.146                        |> fold_rev mk_forall (fvar :: qs)
   7.147 @@ -424,7 +420,8 @@
   7.148      let
   7.149        val f_def = 
   7.150            Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
   7.151 -                                Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G))
   7.152 +                                Abs ("y", ranT, G $ Bound 1 $ Bound 0))
   7.153 +              |> Envir.beta_norm (* Fixme: LocalTheory.def does not work if not beta-normal *)
   7.154            
   7.155        val ((f, (_, f_defthm)), lthy) = LocalTheory.def ((fname ^ "C", mixfix), ((fdefname, []), f_def)) lthy
   7.156      in
   7.157 @@ -435,11 +432,11 @@
   7.158  fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy =
   7.159      let
   7.160  
   7.161 -      val RT = mk_relT (domT, domT)
   7.162 +      val RT = domT --> domT --> boolT
   7.163        val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)]))
   7.164  
   7.165        fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
   7.166 -          mk_relmem (rcarg, lhs) Rvar
   7.167 +          Trueprop (Rvar $ rcarg $ lhs)
   7.168                      |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
   7.169                      |> fold_rev (curry Logic.mk_implies) gs
   7.170                      |> fold_rev (mk_forall o Free) rcfix
   7.171 @@ -465,7 +462,7 @@
   7.172                  x = Free (x, domT),
   7.173                  z = Free (z, domT),
   7.174                  a = Free (a, domT),
   7.175 -                D = Free (D, HOLogic.mk_setT domT),
   7.176 +                D = Free (D, domT --> boolT),
   7.177                  P = Free (P, domT --> boolT),
   7.178                  Pbool = Free (Pbool, boolT),
   7.179                  fvar = fvar,
   7.180 @@ -521,7 +518,7 @@
   7.181        val ((R, RIntro_thmss, R_elim), lthy) = 
   7.182            define_recursion_relation (defname ^ "_rel") domT ranT fvar f abstract_qglrs clauses RCss lthy
   7.183  
   7.184 -      val dom_abbrev = Logic.mk_equals (Free (defname ^ "_dom", fastype_of (mk_acc domT R)), mk_acc domT R)
   7.185 +      val dom_abbrev = Logic.mk_equals (Free (defname ^ "_dom", domT --> boolT), mk_acc domT R)
   7.186        val lthy = Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)] lthy
   7.187  
   7.188        val newthy = ProofContext.theory_of lthy
     8.1 --- a/src/HOL/Tools/function_package/fundef_proof.ML	Wed Oct 18 10:15:39 2006 +0200
     8.2 +++ b/src/HOL/Tools/function_package/fundef_proof.ML	Wed Oct 18 16:13:03 2006 +0200
     8.3 @@ -18,21 +18,24 @@
     8.4  structure FundefProof : FUNDEF_PROOF = 
     8.5  struct
     8.6  
     8.7 +open FundefLib
     8.8  open FundefCommon
     8.9  open FundefAbbrev
    8.10  
    8.11  (* Theory dependencies *)
    8.12  val subsetD = thm "subsetD"
    8.13 -val subset_refl = thm "subset_refl"
    8.14  val split_apply = thm "Product_Type.split"
    8.15 -val wf_induct_rule = thm "wf_induct_rule";
    8.16 +val wf_induct_rule = thm "FunDef.wfP_induct_rule";
    8.17  val Pair_inject = thm "Product_Type.Pair_inject";
    8.18  
    8.19 -val acc_induct_rule = thm "Accessible_Part.acc_induct_rule"
    8.20 -val acc_downward = thm "Accessible_Part.acc_downward"
    8.21 -val accI = thm "Accessible_Part.accI"
    8.22 +val wf_in_rel = thm "FunDef.wf_in_rel";
    8.23 +val in_rel_def = thm "FunDef.in_rel_def";
    8.24  
    8.25 -val acc_subset_induct = thm "Accessible_Part.acc_subset_induct"
    8.26 +val acc_induct_rule = thm "FunDef.accP_induct_rule"
    8.27 +val acc_downward = thm "FunDef.accP_downward"
    8.28 +val accI = thm "FunDef.accPI"
    8.29 +
    8.30 +val acc_subset_induct = thm "FunDef.accP_subset_induct"
    8.31  
    8.32  val conjunctionD1 = thm "conjunctionD1"
    8.33  val conjunctionD2 = thm "conjunctionD2"
    8.34 @@ -43,18 +46,18 @@
    8.35  	val Globals {domT, z, ...} = globals
    8.36  
    8.37  	val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause
    8.38 -	val lhs_acc = cterm_of thy (Trueprop (mk_mem (lhs, mk_acc domT R))) (* "lhs : acc R" *)
    8.39 -	val z_smaller = cterm_of thy (Trueprop (mk_relmemT domT domT (z, lhs) R)) (* "(z, lhs) : R" *)
    8.40 +	val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
    8.41 +	val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
    8.42      in
    8.43  	((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
    8.44 -	    |> (fn it => it COMP graph_is_function)
    8.45 -	    |> implies_intr z_smaller
    8.46 -	    |> forall_intr (cterm_of thy z)
    8.47 -	    |> (fn it => it COMP valthm)
    8.48 -	    |> implies_intr lhs_acc 
    8.49 -	    |> asm_simplify (HOL_basic_ss addsimps [f_iff])
    8.50 -            |> fold_rev (implies_intr o cprop_of) ags
    8.51 -            |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
    8.52 +	  |> (fn it => it COMP graph_is_function)
    8.53 +	  |> implies_intr z_smaller
    8.54 +	  |> forall_intr (cterm_of thy z)
    8.55 +	  |> (fn it => it COMP valthm)
    8.56 +	  |> implies_intr lhs_acc 
    8.57 +	  |> asm_simplify (HOL_basic_ss addsimps [f_iff])
    8.58 +          |> fold_rev (implies_intr o cprop_of) ags
    8.59 +          |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
    8.60      end
    8.61  
    8.62  
    8.63 @@ -64,22 +67,22 @@
    8.64  	val Globals {domT, x, z, a, P, D, ...} = globals
    8.65          val acc_R = mk_acc domT R
    8.66  
    8.67 -	val x_D = assume (cterm_of thy (Trueprop (mk_mem (x, D))))
    8.68 -	val a_D = cterm_of thy (Trueprop (mk_mem (a, D)))
    8.69 +	val x_D = assume (cterm_of thy (Trueprop (D $ x)))
    8.70 +	val a_D = cterm_of thy (Trueprop (D $ a))
    8.71  
    8.72 -	val D_subset = cterm_of thy (Trueprop (mk_subset domT D acc_R))
    8.73 +	val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x)))
    8.74  
    8.75  	val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
    8.76  	    mk_forall x
    8.77 -		      (mk_forall z (Logic.mk_implies (Trueprop (mk_mem (x, D)),
    8.78 -						      Logic.mk_implies (mk_relmem (z, x) R,
    8.79 -									Trueprop (mk_mem (z, D))))))
    8.80 +		      (mk_forall z (Logic.mk_implies (Trueprop (D $ x),
    8.81 +						      Logic.mk_implies (Trueprop (R $ z $ x),
    8.82 +									Trueprop (D $ z)))))
    8.83  		      |> cterm_of thy
    8.84  
    8.85  
    8.86  	(* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
    8.87  	val ihyp = all domT $ Abs ("z", domT, 
    8.88 -				   implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R)
    8.89 +				   implies $ Trueprop (R $ Bound 0 $ x)
    8.90  					   $ Trueprop (P $ Bound 0))
    8.91  		       |> cterm_of thy
    8.92  
    8.93 @@ -105,7 +108,7 @@
    8.94  		val step = Trueprop (P $ lhs)
    8.95  				    |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
    8.96  				    |> fold_rev (curry Logic.mk_implies) gs
    8.97 -				    |> curry Logic.mk_implies (Trueprop (mk_mem (lhs, D)))
    8.98 +				    |> curry Logic.mk_implies (Trueprop (D $ lhs))
    8.99  				    |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   8.100  				    |> cterm_of thy
   8.101  			   
   8.102 @@ -152,10 +155,10 @@
   8.103  	    subset_induct_rule
   8.104  		|> forall_intr (cterm_of thy D)
   8.105  		|> forall_elim (cterm_of thy acc_R)
   8.106 -		|> (curry op COMP) subset_refl
   8.107 +		|> assume_tac 1 |> Seq.hd
   8.108  		|> (curry op COMP) (acc_downward
   8.109  					|> (instantiate' [SOME (ctyp_of thy domT)]
   8.110 -							 (map (SOME o cterm_of thy) [x, R, z]))
   8.111 +							 (map (SOME o cterm_of thy) [R, x, z]))
   8.112  					|> forall_intr (cterm_of thy z)
   8.113  					|> forall_intr (cterm_of thy x))
   8.114  		|> forall_intr (cterm_of thy a)
   8.115 @@ -172,7 +175,7 @@
   8.116  	val Globals {z, domT, ...} = globals
   8.117  	val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...}, 
   8.118                          qglr = (oqs, _, _, _), ...} = clause
   8.119 -	val goal = (HOLogic.mk_Trueprop (HOLogic.mk_mem (lhs, mk_acc domT R)))
   8.120 +	val goal = Trueprop (mk_acc domT R $ lhs)
   8.121                       |> fold_rev (curry Logic.mk_implies) gs
   8.122                       |> cterm_of thy
   8.123      in
   8.124 @@ -199,7 +202,7 @@
   8.125  	    let
   8.126  		val used = map (fn ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub)
   8.127  
   8.128 -		val hyp = mk_relmem (arg, lhs) R'
   8.129 +		val hyp = Trueprop (R' $ arg $ lhs)
   8.130  				    |> fold_rev (curry Logic.mk_implies o prop_of) used
   8.131  				    |> FundefCtxTree.export_term (fixes, map prop_of assumes) 
   8.132  				    |> fold_rev (curry Logic.mk_implies o prop_of) ags
   8.133 @@ -222,11 +225,12 @@
   8.134  				     |> implies_intr (cprop_of case_hyp)
   8.135  				     |> implies_intr z_eq_arg
   8.136  
   8.137 -		val zx_eq_arg_lhs = cterm_of thy (Trueprop (mk_eq (mk_prod (z,x), mk_prod (arg,lhs))))
   8.138 +                val z_eq_arg = assume (cterm_of thy (Trueprop (mk_eq (z, arg))))
   8.139 +                val x_eq_lhs = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
   8.140  
   8.141 -		val ethm = (z_acc COMP (assume zx_eq_arg_lhs COMP Pair_inject))
   8.142 +		val ethm = (z_acc OF [z_eq_arg, x_eq_lhs])
   8.143  			       |> FundefCtxTree.export_thm thy (fixes, 
   8.144 -                                                                (term_of zx_eq_arg_lhs) :: map prop_of (ags @ assumes))
   8.145 +                                                                prop_of z_eq_arg :: prop_of x_eq_lhs :: map prop_of (ags @ assumes))
   8.146                                 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   8.147  
   8.148  		val sub' = sub @ [(([],[]), acc)]
   8.149 @@ -246,36 +250,43 @@
   8.150  
   8.151  	val R' = Free ("R", fastype_of R)
   8.152  
   8.153 -	val wfR' = cterm_of thy (Trueprop (Const ("Wellfounded_Recursion.wf", mk_relT (domT, domT) --> boolT) $ R')) (* "wf R'" *)
   8.154 +        val Rrel = Free ("R", mk_relT (domT, domT))
   8.155 +        val inrel_R = Const ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) $ Rrel
   8.156 +
   8.157 +	val wfR' = cterm_of thy (Trueprop (Const ("FunDef.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
   8.158  
   8.159  	(* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
   8.160  	val ihyp = all domT $ Abs ("z", domT, 
   8.161 -				   implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R')
   8.162 -					   $ Trueprop ((Const ("op :", [domT, HOLogic.mk_setT domT] ---> boolT))
   8.163 -							   $ Bound 0 $ acc_R))
   8.164 +				   implies $ Trueprop (R' $ Bound 0 $ x)
   8.165 +					   $ Trueprop (acc_R $ Bound 0))
   8.166  		       |> cterm_of thy
   8.167  
   8.168  	val ihyp_a = assume ihyp |> forall_elim_vars 0
   8.169  
   8.170 -	val z_ltR_x = cterm_of thy (mk_relmem (z, x) R) (* "(z, x) : R" *)
   8.171 +	val R_z_x = cterm_of thy (Trueprop (R $ z $ x)) 
   8.172  
   8.173  	val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
   8.174      in
   8.175  	R_cases
   8.176 -            |> forall_elim (cterm_of thy (mk_prod (z,x)))
   8.177 -            |> forall_elim (cterm_of thy (mk_mem (z, acc_R)))
   8.178 -	    |> curry op COMP (assume z_ltR_x)
   8.179 +            |> forall_elim (cterm_of thy z)
   8.180 +            |> forall_elim (cterm_of thy x)
   8.181 +            |> forall_elim (cterm_of thy (acc_R $ z))
   8.182 +	    |> curry op COMP (assume R_z_x)
   8.183  	    |> fold_rev (curry op COMP) cases
   8.184 -	    |> implies_intr z_ltR_x
   8.185 +	    |> implies_intr R_z_x
   8.186  	    |> forall_intr (cterm_of thy z)
   8.187  	    |> (fn it => it COMP accI)
   8.188  	    |> implies_intr ihyp
   8.189  	    |> forall_intr (cterm_of thy x)
   8.190  	    |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
   8.191 -	    |> implies_elim_swp (assume wfR')
   8.192 +	    |> curry op RS (assume wfR')
   8.193  	    |> fold implies_intr hyps
   8.194  	    |> implies_intr wfR'
   8.195  	    |> forall_intr (cterm_of thy R')
   8.196 +            |> forall_elim (cterm_of thy (inrel_R))
   8.197 +            |> curry op RS wf_in_rel
   8.198 +            |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
   8.199 +	    |> forall_intr (cterm_of thy Rrel)
   8.200      end
   8.201  
   8.202  
     9.1 --- a/src/HOL/Tools/function_package/inductive_wrap.ML	Wed Oct 18 10:15:39 2006 +0200
     9.2 +++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Wed Oct 18 16:13:03 2006 +0200
     9.3 @@ -30,81 +30,61 @@
     9.4  structure FundefInductiveWrap =
     9.5  struct
     9.6  
     9.7 -
     9.8 -fun inst_forall (Free (n,_)) (_ $ Abs (_, T, b)) = subst_bound (Free (n, T), b)
     9.9 -  | inst_forall t1 t2 = sys_error ((Sign.string_of_term (the_context ()) t1))
    9.10 -
    9.11 -fun permute_bounds_in_premises thy [] impl = impl
    9.12 -  | permute_bounds_in_premises thy ((oldvs, newvs) :: perms) impl =
    9.13 -    let
    9.14 -      val (prem, concl) = dest_implies (cprop_of impl)
    9.15 +open FundefLib
    9.16  
    9.17 -      val newprem = term_of prem
    9.18 -                      |> fold inst_forall oldvs
    9.19 -                      |> fold_rev mk_forall newvs
    9.20 -                      |> cterm_of thy
    9.21 +fun requantify ctxt lfix (qs, t) thm =
    9.22 +    let
    9.23 +      val thy = theory_of_thm (print thm)
    9.24 +      val frees = frees_in_term ctxt t 
    9.25 +                                  |> remove (op =) lfix
    9.26 +      val vars = Term.add_vars (prop_of thm) [] |> rev
    9.27 +                 
    9.28 +      val varmap = frees ~~ vars
    9.29      in
    9.30 -      assume newprem
    9.31 -             |> fold (forall_elim o cterm_of thy) newvs
    9.32 -             |> fold_rev (forall_intr o cterm_of thy) oldvs
    9.33 -             |> implies_elim impl
    9.34 -             |> permute_bounds_in_premises thy perms
    9.35 -             |> implies_intr newprem
    9.36 -    end
    9.37 -
    9.38 +      fold_rev (fn Free (n, T) => 
    9.39 +                   forall_intr_rename (n, cterm_of thy (Var (the_default (("",0), T) (AList.lookup (op =) varmap (n, T))))))
    9.40 +               qs
    9.41 +               thm
    9.42 +    end             
    9.43 +  
    9.44 +  
    9.45  
    9.46  fun inductive_def defs (((R, T), mixfix), lthy) =
    9.47      let
    9.48 -      fun wrap1 thy =
    9.49 -          let
    9.50 -            val thy = Sign.add_consts_i [(R, T, mixfix)] thy
    9.51 -            val RC = Const (Sign.full_name thy R, T)
    9.52 -
    9.53 -            val cdefs = map (Pattern.rewrite_term thy [(Free (R, T), RC)] []) defs
    9.54 -            val qdefs = map dest_all_all cdefs
    9.55 -
    9.56 -            val (thy, {intrs = intrs_gen, elims = [elim_gen], ...}) =
    9.57 -                OldInductivePackage.add_inductive_i true (*verbose*)
    9.58 -                                                 false (* dont add_consts *)
    9.59 -                                                 "" (* no altname *)
    9.60 -                                                 false (* no coind *)
    9.61 -                                                 false (* elims, please *)
    9.62 -                                                 false (* induction thm please *)
    9.63 -                                                 [RC] (* the constant *)
    9.64 -                                                 (map (fn (_,t) => (("", t),[])) qdefs) (* the intros *)
    9.65 -                                                 [] (* no special monos *)
    9.66 -                                                 thy
    9.67 -
    9.68 -            val perms = map (fn (qs, t) => ((term_frees t) inter qs, qs)) qdefs
    9.69 +      val qdefs = map dest_all_all defs
    9.70 +                  
    9.71 +      val (lthy, {intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], ...}) =
    9.72 +          InductivePackage.add_inductive_i true (*verbose*)
    9.73 +                                           "" (* no altname *)
    9.74 +                                           false (* no coind *)
    9.75 +                                           false (* elims, please *)
    9.76 +                                           false (* induction thm please *)
    9.77 +                                           [(R, SOME T, NoSyn)] (* the relation *)
    9.78 +                                           [] (* no parameters *)
    9.79 +                                           (map (fn t => (("", []), t)) defs) (* the intros *)
    9.80 +                                           [] (* no special monos *)
    9.81 +                                           lthy
    9.82  
    9.83 -            fun inst (qs, _) intr_gen =
    9.84 -                intr_gen
    9.85 -                  |> Thm.freezeT
    9.86 -                  |> fold_rev (forall_intr o (fn Free (n, T) => cterm_of thy (Var ((n,0), T)))) qs
    9.87 -
    9.88 -
    9.89 -            val a = cterm_of thy (Free ("a0123", HOLogic.dest_setT T)) (* Let's just hope there are no clashes :-} *)
    9.90 -            val P = cterm_of thy (Free ("P0123", HOLogic.boolT))
    9.91 +      val thy = ProofContext.theory_of lthy
    9.92                  
    9.93 -            val intrs = map2 inst qdefs intrs_gen
    9.94 +      fun inst qdef intr_gen =
    9.95 +          intr_gen
    9.96 +            |> Thm.freezeT
    9.97 +            |> requantify lthy (R, T) qdef 
    9.98 +          
    9.99 +      val intrs = map2 inst qdefs intrs_gen
   9.100 +                  
   9.101 +      val elim = elim_gen
   9.102 +                   |> Thm.freezeT
   9.103 +                   |> forall_intr_vars (* FIXME... *)
   9.104  
   9.105 -            val elim = elim_gen
   9.106 -                         |> Thm.freezeT
   9.107 -                         |> forall_intr_vars (* FIXME... *)
   9.108 -                         |> forall_elim a
   9.109 -                         |> forall_elim P
   9.110 -                         |> permute_bounds_in_premises thy (([],[]) :: perms)
   9.111 -                         |> forall_intr P
   9.112 -                         |> forall_intr a
   9.113 -          in
   9.114 -            ((RC, (intrs, elim)), thy)
   9.115 -          end
   9.116 -
   9.117 -      val ((RC, (intrs, elim)), lthy) = LocalTheory.theory_result wrap1 lthy
   9.118 +      val Rdef_real = prop_of (Thm.freezeT elim_gen)
   9.119 +                       |> Logic.dest_implies |> fst
   9.120 +                       |> Term.strip_comb |> snd |> hd (* Trueprop *)
   9.121 +                       |> Term.strip_comb |> fst
   9.122      in
   9.123 -      (intrs, (RC, elim, lthy))
   9.124 +      (intrs, (Rdef_real, elim, lthy))
   9.125      end
   9.126 -
   9.127 -
   9.128 +    
   9.129  end
   9.130  
    10.1 --- a/src/HOL/Tools/function_package/mutual.ML	Wed Oct 18 10:15:39 2006 +0200
    10.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Wed Oct 18 16:13:03 2006 +0200
    10.3 @@ -27,6 +27,7 @@
    10.4  structure FundefMutual: FUNDEF_MUTUAL =
    10.5  struct
    10.6  
    10.7 +open FundefLib
    10.8  open FundefCommon
    10.9  
   10.10  (* Theory dependencies *)
    11.1 --- a/src/HOL/Tools/function_package/pattern_split.ML	Wed Oct 18 10:15:39 2006 +0200
    11.2 +++ b/src/HOL/Tools/function_package/pattern_split.ML	Wed Oct 18 16:13:03 2006 +0200
    11.3 @@ -21,6 +21,7 @@
    11.4  structure FundefSplit : FUNDEF_SPLIT =
    11.5  struct
    11.6  
    11.7 +open FundefLib
    11.8  
    11.9  (* We use proof context for the variable management *)
   11.10  (* FIXME: no __ *)
    12.1 --- a/src/HOL/Tools/function_package/termination.ML	Wed Oct 18 10:15:39 2006 +0200
    12.2 +++ b/src/HOL/Tools/function_package/termination.ML	Wed Oct 18 16:13:03 2006 +0200
    12.3 @@ -17,6 +17,7 @@
    12.4  struct
    12.5  
    12.6  
    12.7 +open FundefLib
    12.8  open FundefCommon
    12.9  open FundefAbbrev
   12.10  
   12.11 @@ -25,7 +26,7 @@
   12.12  	val domT = domain_type (fastype_of f)
   12.13  	val x = Free ("x", domT)
   12.14      in
   12.15 -      Trueprop (mk_mem (x, Const (acc_const_name, fastype_of R --> HOLogic.mk_setT domT) $ R))
   12.16 +      Trueprop (mk_acc domT R $ x)
   12.17      end
   12.18  
   12.19  fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom =
    13.1 --- a/src/HOL/ex/Fundefs.thy	Wed Oct 18 10:15:39 2006 +0200
    13.2 +++ b/src/HOL/ex/Fundefs.thy	Wed Oct 18 16:13:03 2006 +0200
    13.3 @@ -11,7 +11,6 @@
    13.4  
    13.5  section {* Very basic *}
    13.6  
    13.7 -
    13.8  fun fib :: "nat \<Rightarrow> nat"
    13.9  where
   13.10    "fib 0 = 1"
   13.11 @@ -58,7 +57,7 @@
   13.12  | "nz (Suc x) = nz (nz x)"
   13.13  
   13.14  lemma nz_is_zero: -- {* A lemma we need to prove termination *}
   13.15 -  assumes trm: "x \<in> nz_dom"
   13.16 +  assumes trm: "nz_dom x"
   13.17    shows "nz x = 0"
   13.18  using trm
   13.19  by induct auto
   13.20 @@ -72,14 +71,14 @@
   13.21  
   13.22  text {* Here comes McCarthy's 91-function *}
   13.23  
   13.24 +
   13.25  fun f91 :: "nat => nat"
   13.26  where
   13.27    "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
   13.28  
   13.29 -
   13.30  (* Prove a lemma before attempting a termination proof *)
   13.31  lemma f91_estimate: 
   13.32 -  assumes trm: "n : f91_dom" 
   13.33 +  assumes trm: "f91_dom n" 
   13.34    shows "n < f91 n + 11"
   13.35  using trm by induct auto
   13.36  
   13.37 @@ -91,7 +90,7 @@
   13.38    fix n::nat assume "~ 100 < n" (* Inner call *)
   13.39    thus "(n + 11, n) : ?R" by simp 
   13.40  
   13.41 -  assume inner_trm: "n + 11 : f91_dom" (* Outer call *)
   13.42 +  assume inner_trm: "f91_dom (n + 11)" (* Outer call *)
   13.43    with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
   13.44    with `~ 100 < n` show "(f91 (n + 11), n) : ?R" by simp 
   13.45  qed