1.1 --- a/src/HOL/FunDef.thy Mon Jan 22 16:53:33 2007 +0100
1.2 +++ b/src/HOL/FunDef.thy Mon Jan 22 17:29:43 2007 +0100
1.3 @@ -13,13 +13,11 @@
1.4 ("Tools/function_package/fundef_lib.ML")
1.5 ("Tools/function_package/inductive_wrap.ML")
1.6 ("Tools/function_package/context_tree.ML")
1.7 -("Tools/function_package/fundef_prep.ML")
1.8 -("Tools/function_package/fundef_proof.ML")
1.9 +("Tools/function_package/fundef_core.ML")
1.10 ("Tools/function_package/termination.ML")
1.11 ("Tools/function_package/mutual.ML")
1.12 ("Tools/function_package/pattern_split.ML")
1.13 ("Tools/function_package/fundef_package.ML")
1.14 -(*("Tools/function_package/fundef_datatype.ML")*)
1.15 ("Tools/function_package/auto_term.ML")
1.16 begin
1.17
1.18 @@ -71,6 +69,27 @@
1.19 done
1.20
1.21
1.22 +lemma not_accP_down:
1.23 + assumes na: "\<not> accP R x"
1.24 + obtains z where "R z x" and "\<not>accP R z"
1.25 +proof -
1.26 + assume a: "\<And>z. \<lbrakk>R z x; \<not> accP R z\<rbrakk> \<Longrightarrow> thesis"
1.27 +
1.28 + show thesis
1.29 + proof (cases "\<forall>z. R z x \<longrightarrow> accP R z")
1.30 + case True
1.31 + hence "\<And>z. R z x \<Longrightarrow> accP R z" by auto
1.32 + hence "accP R x"
1.33 + by (rule accPI)
1.34 + with na show thesis ..
1.35 + next
1.36 + case False then obtain z where "R z x" and "\<not>accP R z"
1.37 + by auto
1.38 + with a show thesis .
1.39 + qed
1.40 +qed
1.41 +
1.42 +
1.43 lemma accP_subset:
1.44 assumes sub: "\<And>x y. R1 x y \<Longrightarrow> R2 x y"
1.45 shows "\<And>x. accP R2 x \<Longrightarrow> accP R1 x"
1.46 @@ -195,8 +214,7 @@
1.47 use "Tools/function_package/fundef_lib.ML"
1.48 use "Tools/function_package/inductive_wrap.ML"
1.49 use "Tools/function_package/context_tree.ML"
1.50 -use "Tools/function_package/fundef_prep.ML"
1.51 -use "Tools/function_package/fundef_proof.ML"
1.52 +use "Tools/function_package/fundef_core.ML"
1.53 use "Tools/function_package/termination.ML"
1.54 use "Tools/function_package/mutual.ML"
1.55 use "Tools/function_package/pattern_split.ML"
2.1 --- a/src/HOL/IsaMakefile Mon Jan 22 16:53:33 2007 +0100
2.2 +++ b/src/HOL/IsaMakefile Mon Jan 22 17:29:43 2007 +0100
2.3 @@ -107,8 +107,7 @@
2.4 Tools/function_package/fundef_datatype.ML \
2.5 Tools/function_package/fundef_lib.ML \
2.6 Tools/function_package/fundef_package.ML \
2.7 - Tools/function_package/fundef_prep.ML \
2.8 - Tools/function_package/fundef_proof.ML \
2.9 + Tools/function_package/fundef_core.ML \
2.10 Tools/function_package/inductive_wrap.ML \
2.11 Tools/function_package/lexicographic_order.ML \
2.12 Tools/function_package/mutual.ML \
3.1 --- a/src/HOL/Tools/function_package/fundef_common.ML Mon Jan 22 16:53:33 2007 +0100
3.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML Mon Jan 22 17:29:43 2007 +0100
3.3 @@ -12,7 +12,6 @@
3.4 (* Theory Dependencies *)
3.5 val acc_const_name = "FunDef.accP"
3.6
3.7 -val domintros = ref true;
3.8 val profile = ref false;
3.9
3.10 fun PROFILE msg = if !profile then timeap_msg msg else I
3.11 @@ -20,6 +19,7 @@
3.12 fun mk_acc domT R =
3.13 Const (acc_const_name, (fastype_of R) --> domT --> HOLogic.boolT) $ R
3.14
3.15 +(* FIXME, unused *)
3.16 val function_name = suffix "C"
3.17 val graph_name = suffix "_graph"
3.18 val rel_name = suffix "_rel"
3.19 @@ -35,163 +35,29 @@
3.20 | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list)
3.21 | RCall of (term * ctx_tree)
3.22
3.23 -type glrs = (term list * term list * term * term) list
3.24
3.25
3.26 -datatype globals =
3.27 - Globals of {
3.28 - fvar: term,
3.29 - domT: typ,
3.30 - ranT: typ,
3.31 - h: term,
3.32 - y: term,
3.33 - x: term,
3.34 - z: term,
3.35 - a:term,
3.36 - P: term,
3.37 - D: term,
3.38 - Pbool:term
3.39 -}
3.40 -
3.41 -
3.42 -datatype rec_call_info =
3.43 - RCInfo of
3.44 - {
3.45 - RIvs: (string * typ) list, (* Call context: fixes and assumes *)
3.46 - CCas: thm list,
3.47 - rcarg: term, (* The recursive argument *)
3.48 -
3.49 - llRI: thm,
3.50 - h_assum: term
3.51 - }
3.52 -
3.53 -
3.54 -datatype clause_context =
3.55 - ClauseContext of
3.56 - {
3.57 - ctxt : Proof.context,
3.58 -
3.59 - qs : term list,
3.60 - gs : term list,
3.61 - lhs: term,
3.62 - rhs: term,
3.63 -
3.64 - cqs: cterm list,
3.65 - ags: thm list,
3.66 - case_hyp : thm
3.67 - }
3.68 -
3.69 -
3.70 -fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =
3.71 - ClauseContext { ctxt = ProofContext.transfer thy ctxt,
3.72 - qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
3.73 -
3.74 -
3.75 -datatype clause_info =
3.76 - ClauseInfo of
3.77 - {
3.78 - no: int,
3.79 - qglr : ((string * typ) list * term list * term * term),
3.80 - cdata : clause_context,
3.81 -
3.82 - tree: ctx_tree,
3.83 - lGI: thm,
3.84 - RCs: rec_call_info list
3.85 - }
3.86 -
3.87 -
3.88 -
3.89 -
3.90 -type qgar = string * (string * typ) list * term list * term list * term
3.91 -
3.92 -fun name_of_fqgar (f, _, _, _, _) = f
3.93 -
3.94 -datatype mutual_part =
3.95 - MutualPart of
3.96 - {
3.97 - fvar : string * typ,
3.98 - cargTs: typ list,
3.99 - pthA: SumTools.sum_path,
3.100 - pthR: SumTools.sum_path,
3.101 - f_def: term,
3.102 -
3.103 - f: term option,
3.104 - f_defthm : thm option
3.105 - }
3.106 -
3.107 -
3.108 -datatype mutual_info =
3.109 - Mutual of
3.110 - {
3.111 - defname: string,
3.112 - fsum_var : string * typ,
3.113 -
3.114 - ST: typ,
3.115 - RST: typ,
3.116 - streeA: SumTools.sum_tree,
3.117 - streeR: SumTools.sum_tree,
3.118 -
3.119 - parts: mutual_part list,
3.120 - fqgars: qgar list,
3.121 - qglrs: ((string * typ) list * term list * term * term) list,
3.122 -
3.123 - fsum : term option
3.124 - }
3.125 -
3.126 -
3.127 -datatype prep_result =
3.128 - Prep of
3.129 - {
3.130 - globals: globals,
3.131 - f: term,
3.132 - G: term,
3.133 - R: term,
3.134 -
3.135 - goal: term,
3.136 - goalI: thm,
3.137 - values: thm list,
3.138 - clauses: clause_info list,
3.139 -
3.140 - R_cases: thm,
3.141 - ex1_iff: thm
3.142 - }
3.143 -
3.144 datatype fundef_result =
3.145 FundefResult of
3.146 {
3.147 f: term,
3.148 - G : term,
3.149 - R : term,
3.150 - completeness : thm,
3.151 -
3.152 - psimps : thm list,
3.153 - subset_pinduct : thm,
3.154 - simple_pinduct : thm,
3.155 - total_intro : thm,
3.156 - dom_intros : thm list
3.157 - }
3.158 -
3.159 -datatype fundef_mresult =
3.160 - FundefMResult of
3.161 - {
3.162 - f: term,
3.163 G: term,
3.164 R: term,
3.165
3.166 psimps : thm list,
3.167 + trsimps : thm list option,
3.168 +
3.169 subset_pinducts : thm list,
3.170 simple_pinducts : thm list,
3.171 cases : thm,
3.172 termination : thm,
3.173 - domintros : thm list
3.174 + domintros : thm list option
3.175 }
3.176
3.177 datatype fundef_context_data =
3.178 FundefCtxData of
3.179 {
3.180 - fixes : ((string * typ) * mixfix) list,
3.181 - spec : ((string * Attrib.src list) * term list) list list,
3.182 - mutual: mutual_info,
3.183 + add_simps : string -> Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
3.184
3.185 f : term,
3.186 R : term,
3.187 @@ -261,6 +127,7 @@
3.188 | Preprocessor of string
3.189 | Target of xstring
3.190 | DomIntros
3.191 + | Tailrec
3.192
3.193 datatype fundef_config
3.194 = FundefConfig of
3.195 @@ -269,23 +136,29 @@
3.196 default: string,
3.197 preprocessor: string option,
3.198 target: xstring option,
3.199 - domintros: bool
3.200 + domintros: bool,
3.201 + tailrec: bool
3.202 }
3.203
3.204
3.205 -val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE, target=NONE, domintros=false }
3.206 -val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE, target=NONE, domintros=false }
3.207 +val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE,
3.208 + target=NONE, domintros=false, tailrec=false }
3.209 +
3.210 +val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE,
3.211 + target=NONE, domintros=false, tailrec=false }
3.212
3.213 -fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target, domintros}) =
3.214 - FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target, domintros=domintros }
3.215 - | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target, domintros}) =
3.216 - FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target, domintros=domintros }
3.217 - | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target, domintros}) =
3.218 - FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target, domintros=domintros }
3.219 - | apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target, domintros }) =
3.220 - FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t, domintros=domintros }
3.221 - | apply_opt Domintros (FundefConfig {sequential, default, preprocessor, target, domintros }) =
3.222 - FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=true }
3.223 +fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) =
3.224 + FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target, domintros=domintros, tailrec=tailrec }
3.225 + | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) =
3.226 + FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target, domintros=domintros, tailrec=tailrec }
3.227 + | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) =
3.228 + FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target, domintros=domintros, tailrec=tailrec }
3.229 + | apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
3.230 + FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t, domintros=domintros, tailrec=tailrec }
3.231 + | apply_opt DomIntros (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
3.232 + FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=true,tailrec=tailrec }
3.233 + | apply_opt Tailrec (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
3.234 + FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=domintros,tailrec=true }
3.235
3.236
3.237 local structure P = OuterParse and K = OuterKeyword in
3.238 @@ -295,29 +168,18 @@
3.239 val option_parser = (P.$$$ "sequential" >> K Sequential)
3.240 || ((P.reserved "default" |-- P.term) >> Default)
3.241 || (P.reserved "domintros" >> K DomIntros)
3.242 + || (P.reserved "tailrec" >> K Tailrec)
3.243 || ((P.$$$ "in" |-- P.xname) >> Target)
3.244
3.245 fun config_parser def = (Scan.optional (P.$$$ "(" |-- P.list1 option_parser --| P.$$$ ")") [])
3.246 >> (fn opts => fold apply_opt opts def)
3.247 +
3.248 end
3.249
3.250
3.251
3.252
3.253
3.254 -
3.255 -
3.256 -
3.257 -
3.258 -
3.259 -
3.260 -
3.261 -
3.262 -
3.263 -
3.264 -
3.265 -
3.266 -
3.267 end
3.268
3.269
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/Tools/function_package/fundef_core.ML Mon Jan 22 17:29:43 2007 +0100
4.3 @@ -0,0 +1,952 @@
4.4 +(* Title: HOL/Tools/function_package/fundef_core.ML
4.5 + ID: $Id$
4.6 + Author: Alexander Krauss, TU Muenchen
4.7 +
4.8 +A package for general recursive function definitions.
4.9 +Main functionality
4.10 +*)
4.11 +
4.12 +signature FUNDEF_CORE =
4.13 +sig
4.14 + val prepare_fundef : FundefCommon.fundef_config
4.15 + -> string (* defname *)
4.16 + -> (string * typ * mixfix) (* defined symbol *)
4.17 + -> ((string * typ) list * term list * term * term) list (* specification *)
4.18 + -> string (* default_value, not parsed yet *)
4.19 + -> local_theory
4.20 +
4.21 + -> (term (* f *)
4.22 + * thm (* goalstate *)
4.23 + * (thm -> FundefCommon.fundef_result) (* continuation *)
4.24 + ) * local_theory
4.25 +
4.26 +end
4.27 +
4.28 +structure FundefCore : FUNDEF_CORE =
4.29 +struct
4.30 +
4.31 +
4.32 +open FundefLib
4.33 +open FundefCommon
4.34 +open FundefAbbrev
4.35 +
4.36 +datatype globals =
4.37 + Globals of {
4.38 + fvar: term,
4.39 + domT: typ,
4.40 + ranT: typ,
4.41 + h: term,
4.42 + y: term,
4.43 + x: term,
4.44 + z: term,
4.45 + a: term,
4.46 + P: term,
4.47 + D: term,
4.48 + Pbool:term
4.49 +}
4.50 +
4.51 +
4.52 +datatype rec_call_info =
4.53 + RCInfo of
4.54 + {
4.55 + RIvs: (string * typ) list, (* Call context: fixes and assumes *)
4.56 + CCas: thm list,
4.57 + rcarg: term, (* The recursive argument *)
4.58 +
4.59 + llRI: thm,
4.60 + h_assum: term
4.61 + }
4.62 +
4.63 +
4.64 +datatype clause_context =
4.65 + ClauseContext of
4.66 + {
4.67 + ctxt : Proof.context,
4.68 +
4.69 + qs : term list,
4.70 + gs : term list,
4.71 + lhs: term,
4.72 + rhs: term,
4.73 +
4.74 + cqs: cterm list,
4.75 + ags: thm list,
4.76 + case_hyp : thm
4.77 + }
4.78 +
4.79 +
4.80 +fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =
4.81 + ClauseContext { ctxt = ProofContext.transfer thy ctxt,
4.82 + qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
4.83 +
4.84 +
4.85 +datatype clause_info =
4.86 + ClauseInfo of
4.87 + {
4.88 + no: int,
4.89 + qglr : ((string * typ) list * term list * term * term),
4.90 + cdata : clause_context,
4.91 +
4.92 + tree: ctx_tree,
4.93 + lGI: thm,
4.94 + RCs: rec_call_info list
4.95 + }
4.96 +
4.97 +
4.98 +(* Theory dependencies. *)
4.99 +val Pair_inject = thm "Product_Type.Pair_inject";
4.100 +
4.101 +val acc_induct_rule = thm "FunDef.accP_induct_rule"
4.102 +
4.103 +val ex1_implies_ex = thm "FunDef.fundef_ex1_existence"
4.104 +val ex1_implies_un = thm "FunDef.fundef_ex1_uniqueness"
4.105 +val ex1_implies_iff = thm "FunDef.fundef_ex1_iff"
4.106 +
4.107 +val acc_downward = thm "FunDef.accP_downward"
4.108 +val accI = thm "FunDef.accPI"
4.109 +val case_split = thm "HOL.case_split_thm"
4.110 +val fundef_default_value = thm "FunDef.fundef_default_value"
4.111 +val not_accP_down = thm "FunDef.not_accP_down"
4.112 +
4.113 +
4.114 +
4.115 +fun find_calls tree =
4.116 + let
4.117 + fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs)
4.118 + | add_Ri _ _ _ _ = raise Match
4.119 + in
4.120 + rev (FundefCtxTree.traverse_tree add_Ri tree [])
4.121 + end
4.122 +
4.123 +
4.124 +(** building proof obligations *)
4.125 +
4.126 +fun mk_compat_proof_obligations domT ranT fvar f glrs =
4.127 + let
4.128 + fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
4.129 + let
4.130 + val shift = incr_boundvars (length qs')
4.131 + in
4.132 + (implies $ Trueprop (eq_const domT $ shift lhs $ lhs')
4.133 + $ Trueprop (eq_const ranT $ shift rhs $ rhs'))
4.134 + |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
4.135 + |> fold_rev (fn (n,T) => fn b => all T $ Abs(n,T,b)) (qs @ qs')
4.136 + |> curry abstract_over fvar
4.137 + |> curry subst_bound f
4.138 + end
4.139 + in
4.140 + map mk_impl (unordered_pairs glrs)
4.141 + end
4.142 +
4.143 +
4.144 +fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
4.145 + let
4.146 + fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
4.147 + Trueprop Pbool
4.148 + |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
4.149 + |> fold_rev (curry Logic.mk_implies) gs
4.150 + |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
4.151 + in
4.152 + Trueprop Pbool
4.153 + |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
4.154 + |> mk_forall_rename ("x", x)
4.155 + |> mk_forall_rename ("P", Pbool)
4.156 + end
4.157 +
4.158 +(** making a context with it's own local bindings **)
4.159 +
4.160 +fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
4.161 + let
4.162 + val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
4.163 + |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
4.164 +
4.165 + val thy = ProofContext.theory_of ctxt'
4.166 +
4.167 + fun inst t = subst_bounds (rev qs, t)
4.168 + val gs = map inst pre_gs
4.169 + val lhs = inst pre_lhs
4.170 + val rhs = inst pre_rhs
4.171 +
4.172 + val cqs = map (cterm_of thy) qs
4.173 + val ags = map (assume o cterm_of thy) gs
4.174 +
4.175 + val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
4.176 + in
4.177 + ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
4.178 + cqs = cqs, ags = ags, case_hyp = case_hyp }
4.179 + end
4.180 +
4.181 +
4.182 +(* lowlevel term function *)
4.183 +fun abstract_over_list vs body =
4.184 + let
4.185 + exception SAME;
4.186 + fun abs lev v tm =
4.187 + if v aconv tm then Bound lev
4.188 + else
4.189 + (case tm of
4.190 + Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
4.191 + | t $ u => (abs lev v t $ (abs lev v u handle SAME => u) handle SAME => t $ abs lev v u)
4.192 + | _ => raise SAME);
4.193 + in
4.194 + fold_index (fn (i,v) => fn t => abs i v t handle SAME => t) vs body
4.195 + end
4.196 +
4.197 +
4.198 +
4.199 +fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
4.200 + let
4.201 + val Globals {h, fvar, x, ...} = globals
4.202 +
4.203 + val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
4.204 + val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
4.205 +
4.206 + (* Instantiate the GIntro thm with "f" and import into the clause context. *)
4.207 + val lGI = GIntro_thm
4.208 + |> forall_elim (cert f)
4.209 + |> fold forall_elim cqs
4.210 + |> fold implies_elim_swp ags
4.211 +
4.212 + fun mk_call_info (rcfix, rcassm, rcarg) RI =
4.213 + let
4.214 + val llRI = RI
4.215 + |> fold forall_elim cqs
4.216 + |> fold (forall_elim o cert o Free) rcfix
4.217 + |> fold implies_elim_swp ags
4.218 + |> fold implies_elim_swp rcassm
4.219 +
4.220 + val h_assum =
4.221 + Trueprop (G $ rcarg $ (h $ rcarg))
4.222 + |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
4.223 + |> fold_rev (mk_forall o Free) rcfix
4.224 + |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
4.225 + |> abstract_over_list (rev qs)
4.226 + in
4.227 + RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
4.228 + end
4.229 +
4.230 + val RC_infos = map2 mk_call_info RCs RIntro_thms
4.231 + in
4.232 + ClauseInfo
4.233 + {
4.234 + no=no,
4.235 + cdata=cdata,
4.236 + qglr=qglr,
4.237 +
4.238 + lGI=lGI,
4.239 + RCs=RC_infos,
4.240 + tree=tree
4.241 + }
4.242 + end
4.243 +
4.244 +
4.245 +
4.246 +
4.247 +
4.248 +
4.249 +
4.250 +(* replace this by a table later*)
4.251 +fun store_compat_thms 0 thms = []
4.252 + | store_compat_thms n thms =
4.253 + let
4.254 + val (thms1, thms2) = chop n thms
4.255 + in
4.256 + (thms1 :: store_compat_thms (n - 1) thms2)
4.257 + end
4.258 +
4.259 +(* expects i <= j *)
4.260 +fun lookup_compat_thm i j cts =
4.261 + nth (nth cts (i - 1)) (j - i)
4.262 +
4.263 +(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
4.264 +(* if j < i, then turn around *)
4.265 +fun get_compat_thm thy cts i j ctxi ctxj =
4.266 + let
4.267 + val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
4.268 + val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
4.269 +
4.270 + val lhsi_eq_lhsj = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj)))
4.271 + in if j < i then
4.272 + let
4.273 + val compat = lookup_compat_thm j i cts
4.274 + in
4.275 + compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
4.276 + |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
4.277 + |> fold implies_elim_swp agsj
4.278 + |> fold implies_elim_swp agsi
4.279 + |> implies_elim_swp ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
4.280 + end
4.281 + else
4.282 + let
4.283 + val compat = lookup_compat_thm i j cts
4.284 + in
4.285 + compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
4.286 + |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
4.287 + |> fold implies_elim_swp agsi
4.288 + |> fold implies_elim_swp agsj
4.289 + |> implies_elim_swp (assume lhsi_eq_lhsj)
4.290 + |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
4.291 + end
4.292 + end
4.293 +
4.294 +
4.295 +
4.296 +
4.297 +(* Generates the replacement lemma in fully quantified form. *)
4.298 +fun mk_replacement_lemma thy h ih_elim clause =
4.299 + let
4.300 + val ClauseInfo {cdata=ClauseContext {qs, lhs, rhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
4.301 +
4.302 + val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
4.303 +
4.304 + val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
4.305 + val h_assums = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
4.306 +
4.307 + val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
4.308 +
4.309 + val (eql, _) = FundefCtxTree.rewrite_by_tree thy h ih_elim_case_inst (Ris ~~ h_assums) tree
4.310 +
4.311 + val replace_lemma = (eql RS meta_eq_to_obj_eq)
4.312 + |> implies_intr (cprop_of case_hyp)
4.313 + |> fold_rev (implies_intr o cprop_of) h_assums
4.314 + |> fold_rev (implies_intr o cprop_of) ags
4.315 + |> fold_rev forall_intr cqs
4.316 + |> Goal.close_result
4.317 + in
4.318 + replace_lemma
4.319 + end
4.320 +
4.321 +
4.322 +fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj =
4.323 + let
4.324 + val Globals {h, y, x, fvar, ...} = globals
4.325 + val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
4.326 + val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
4.327 +
4.328 + val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...}
4.329 + = mk_clause_context x ctxti cdescj
4.330 +
4.331 + val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
4.332 + val compat = get_compat_thm thy compat_store i j cctxi cctxj
4.333 + val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
4.334 +
4.335 + val RLj_import =
4.336 + RLj |> fold forall_elim cqsj'
4.337 + |> fold implies_elim_swp agsj'
4.338 + |> fold implies_elim_swp Ghsj'
4.339 +
4.340 + val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
4.341 + val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
4.342 + in
4.343 + (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
4.344 + |> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
4.345 + |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
4.346 + |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
4.347 + |> fold_rev (implies_intr o cprop_of) Ghsj'
4.348 + |> fold_rev (implies_intr o cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
4.349 + |> implies_intr (cprop_of y_eq_rhsj'h)
4.350 + |> implies_intr (cprop_of lhsi_eq_lhsj')
4.351 + |> fold_rev forall_intr (cterm_of thy h :: cqsj')
4.352 + end
4.353 +
4.354 +
4.355 +
4.356 +fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
4.357 + let
4.358 + val Globals {x, y, ranT, fvar, ...} = globals
4.359 + val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
4.360 + val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
4.361 +
4.362 + val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
4.363 +
4.364 + fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
4.365 + |> fold_rev (implies_intr o cprop_of) CCas
4.366 + |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
4.367 +
4.368 + val existence = fold (curry op COMP o prep_RC) RCs lGI
4.369 +
4.370 + val P = cterm_of thy (mk_eq (y, rhsC))
4.371 + val G_lhs_y = assume (cterm_of thy (Trueprop (G $ lhs $ y)))
4.372 +
4.373 + val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas
4.374 +
4.375 + val uniqueness = G_cases
4.376 + |> forall_elim (cterm_of thy lhs)
4.377 + |> forall_elim (cterm_of thy y)
4.378 + |> forall_elim P
4.379 + |> implies_elim_swp G_lhs_y
4.380 + |> fold implies_elim_swp unique_clauses
4.381 + |> implies_intr (cprop_of G_lhs_y)
4.382 + |> forall_intr (cterm_of thy y)
4.383 +
4.384 + val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
4.385 +
4.386 + val exactly_one =
4.387 + ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
4.388 + |> curry (op COMP) existence
4.389 + |> curry (op COMP) uniqueness
4.390 + |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
4.391 + |> implies_intr (cprop_of case_hyp)
4.392 + |> fold_rev (implies_intr o cprop_of) ags
4.393 + |> fold_rev forall_intr cqs
4.394 +
4.395 + val function_value =
4.396 + existence
4.397 + |> implies_intr ihyp
4.398 + |> implies_intr (cprop_of case_hyp)
4.399 + |> forall_intr (cterm_of thy x)
4.400 + |> forall_elim (cterm_of thy lhs)
4.401 + |> curry (op RS) refl
4.402 + in
4.403 + (exactly_one, function_value)
4.404 + end
4.405 +
4.406 +
4.407 +
4.408 +
4.409 +fun prove_stuff thy congs globals G f R clauses complete compat compat_store G_elim f_def =
4.410 + let
4.411 + val Globals {h, domT, ranT, x, ...} = globals
4.412 +
4.413 + (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
4.414 + val ihyp = all domT $ Abs ("z", domT,
4.415 + implies $ Trueprop (R $ Bound 0 $ x)
4.416 + $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
4.417 + Abs ("y", ranT, G $ Bound 1 $ Bound 0)))
4.418 + |> cterm_of thy
4.419 +
4.420 + val ihyp_thm = assume ihyp |> forall_elim_vars 0
4.421 + val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
4.422 + val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
4.423 +
4.424 + val _ = Output.debug (K "Proving Replacement lemmas...")
4.425 + val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
4.426 +
4.427 + val _ = Output.debug (K "Proving cases for unique existence...")
4.428 + val (ex1s, values) =
4.429 + split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
4.430 +
4.431 + val _ = Output.debug (K "Proving: Graph is a function") (* FIXME: Rewrite this proof. *)
4.432 + val graph_is_function = complete
4.433 + |> forall_elim_vars 0
4.434 + |> fold (curry op COMP) ex1s
4.435 + |> implies_intr (ihyp)
4.436 + |> implies_intr (cterm_of thy (Trueprop (mk_acc domT R $ x)))
4.437 + |> forall_intr (cterm_of thy x)
4.438 + |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
4.439 + |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
4.440 +
4.441 + val goalstate = Conjunction.intr graph_is_function complete
4.442 + |> Goal.close_result
4.443 + |> Goal.protect
4.444 + |> fold_rev (implies_intr o cprop_of) compat
4.445 + |> implies_intr (cprop_of complete)
4.446 + in
4.447 + (goalstate, values)
4.448 + end
4.449 +
4.450 +
4.451 +fun define_graph Gname fvar domT ranT clauses RCss lthy =
4.452 + let
4.453 + val GT = domT --> ranT --> boolT
4.454 + val Gvar = Free (the_single (Variable.variant_frees lthy [] [(Gname, GT)]))
4.455 +
4.456 + fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
4.457 + let
4.458 + fun mk_h_assm (rcfix, rcassm, rcarg) =
4.459 + Trueprop (Gvar $ rcarg $ (fvar $ rcarg))
4.460 + |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
4.461 + |> fold_rev (mk_forall o Free) rcfix
4.462 + in
4.463 + Trueprop (Gvar $ lhs $ rhs)
4.464 + |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
4.465 + |> fold_rev (curry Logic.mk_implies) gs
4.466 + |> fold_rev mk_forall (fvar :: qs)
4.467 + end
4.468 +
4.469 + val G_intros = map2 mk_GIntro clauses RCss
4.470 +
4.471 + val (GIntro_thms, (G, G_elim, G_induct, lthy)) =
4.472 + FundefInductiveWrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy)
4.473 + in
4.474 + ((G, GIntro_thms, G_elim, G_induct), lthy)
4.475 + end
4.476 +
4.477 +
4.478 +
4.479 +fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
4.480 + let
4.481 + val f_def =
4.482 + Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
4.483 + Abs ("y", ranT, G $ Bound 1 $ Bound 0))
4.484 + |> Envir.beta_norm (* FIXME: LocalTheory.def does not work if not beta-normal *)
4.485 +
4.486 + val ((f, (_, f_defthm)), lthy) =
4.487 + LocalTheory.def Thm.internalK ((fname ^ "C", mixfix), ((fdefname, []), f_def)) lthy
4.488 + in
4.489 + ((f, f_defthm), lthy)
4.490 + end
4.491 +
4.492 +
4.493 +fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy =
4.494 + let
4.495 +
4.496 + val RT = domT --> domT --> boolT
4.497 + val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)]))
4.498 +
4.499 + fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
4.500 + Trueprop (Rvar $ rcarg $ lhs)
4.501 + |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
4.502 + |> fold_rev (curry Logic.mk_implies) gs
4.503 + |> fold_rev (mk_forall o Free) rcfix
4.504 + |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
4.505 + (* "!!qs xs. CS ==> G => (r, lhs) : R" *)
4.506 +
4.507 + val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
4.508 +
4.509 + val (RIntro_thmss, (R, R_elim, _, lthy)) =
4.510 + fold_burrow FundefInductiveWrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy)
4.511 + in
4.512 + ((R, RIntro_thmss, R_elim), lthy)
4.513 + end
4.514 +
4.515 +
4.516 +fun fix_globals domT ranT fvar ctxt =
4.517 + let
4.518 + val ([h, y, x, z, a, D, P, Pbool],ctxt') =
4.519 + Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
4.520 + in
4.521 + (Globals {h = Free (h, domT --> ranT),
4.522 + y = Free (y, ranT),
4.523 + x = Free (x, domT),
4.524 + z = Free (z, domT),
4.525 + a = Free (a, domT),
4.526 + D = Free (D, domT --> boolT),
4.527 + P = Free (P, domT --> boolT),
4.528 + Pbool = Free (Pbool, boolT),
4.529 + fvar = fvar,
4.530 + domT = domT,
4.531 + ranT = ranT
4.532 + },
4.533 + ctxt')
4.534 + end
4.535 +
4.536 +
4.537 +
4.538 +fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
4.539 + let
4.540 + fun inst_term t = subst_bound(f, abstract_over (fvar, t))
4.541 + in
4.542 + (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
4.543 + end
4.544 +
4.545 +
4.546 +
4.547 +(**********************************************************
4.548 + * PROVING THE RULES
4.549 + **********************************************************)
4.550 +
4.551 +fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
4.552 + let
4.553 + val Globals {domT, z, ...} = globals
4.554 +
4.555 + fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
4.556 + let
4.557 + val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
4.558 + val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
4.559 + in
4.560 + ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
4.561 + |> (fn it => it COMP graph_is_function)
4.562 + |> implies_intr z_smaller
4.563 + |> forall_intr (cterm_of thy z)
4.564 + |> (fn it => it COMP valthm)
4.565 + |> implies_intr lhs_acc
4.566 + |> asm_simplify (HOL_basic_ss addsimps [f_iff])
4.567 + |> fold_rev (implies_intr o cprop_of) ags
4.568 + |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
4.569 + end
4.570 + in
4.571 + map2 mk_psimp clauses valthms
4.572 + end
4.573 +
4.574 +
4.575 +(** Induction rule **)
4.576 +
4.577 +
4.578 +val acc_subset_induct = thm "FunDef.accP_subset_induct"
4.579 +
4.580 +fun mk_partial_induct_rule thy globals R complete_thm clauses =
4.581 + let
4.582 + val Globals {domT, x, z, a, P, D, ...} = globals
4.583 + val acc_R = mk_acc domT R
4.584 +
4.585 + val x_D = assume (cterm_of thy (Trueprop (D $ x)))
4.586 + val a_D = cterm_of thy (Trueprop (D $ a))
4.587 +
4.588 + val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x)))
4.589 +
4.590 + val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
4.591 + mk_forall x
4.592 + (mk_forall z (Logic.mk_implies (Trueprop (D $ x),
4.593 + Logic.mk_implies (Trueprop (R $ z $ x),
4.594 + Trueprop (D $ z)))))
4.595 + |> cterm_of thy
4.596 +
4.597 +
4.598 + (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
4.599 + val ihyp = all domT $ Abs ("z", domT,
4.600 + implies $ Trueprop (R $ Bound 0 $ x)
4.601 + $ Trueprop (P $ Bound 0))
4.602 + |> cterm_of thy
4.603 +
4.604 + val aihyp = assume ihyp
4.605 +
4.606 + fun prove_case clause =
4.607 + let
4.608 + val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs,
4.609 + qglr = (oqs, _, _, _), ...} = clause
4.610 +
4.611 + val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
4.612 + val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
4.613 + val sih = full_simplify replace_x_ss aihyp
4.614 +
4.615 + fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
4.616 + sih |> forall_elim (cterm_of thy rcarg)
4.617 + |> implies_elim_swp llRI
4.618 + |> fold_rev (implies_intr o cprop_of) CCas
4.619 + |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
4.620 +
4.621 + val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *)
4.622 +
4.623 + val step = Trueprop (P $ lhs)
4.624 + |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
4.625 + |> fold_rev (curry Logic.mk_implies) gs
4.626 + |> curry Logic.mk_implies (Trueprop (D $ lhs))
4.627 + |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
4.628 + |> cterm_of thy
4.629 +
4.630 + val P_lhs = assume step
4.631 + |> fold forall_elim cqs
4.632 + |> implies_elim_swp lhs_D
4.633 + |> fold_rev implies_elim_swp ags
4.634 + |> fold implies_elim_swp P_recs
4.635 +
4.636 + val res = cterm_of thy (Trueprop (P $ x))
4.637 + |> Simplifier.rewrite replace_x_ss
4.638 + |> symmetric (* P lhs == P x *)
4.639 + |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
4.640 + |> implies_intr (cprop_of case_hyp)
4.641 + |> fold_rev (implies_intr o cprop_of) ags
4.642 + |> fold_rev forall_intr cqs
4.643 + in
4.644 + (res, step)
4.645 + end
4.646 +
4.647 + val (cases, steps) = split_list (map prove_case clauses)
4.648 +
4.649 + val istep = complete_thm
4.650 + |> forall_elim_vars 0
4.651 + |> fold (curry op COMP) cases (* P x *)
4.652 + |> implies_intr ihyp
4.653 + |> implies_intr (cprop_of x_D)
4.654 + |> forall_intr (cterm_of thy x)
4.655 +
4.656 + val subset_induct_rule =
4.657 + acc_subset_induct
4.658 + |> (curry op COMP) (assume D_subset)
4.659 + |> (curry op COMP) (assume D_dcl)
4.660 + |> (curry op COMP) (assume a_D)
4.661 + |> (curry op COMP) istep
4.662 + |> fold_rev implies_intr steps
4.663 + |> implies_intr a_D
4.664 + |> implies_intr D_dcl
4.665 + |> implies_intr D_subset
4.666 +
4.667 + val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
4.668 +
4.669 + val simple_induct_rule =
4.670 + subset_induct_rule
4.671 + |> forall_intr (cterm_of thy D)
4.672 + |> forall_elim (cterm_of thy acc_R)
4.673 + |> assume_tac 1 |> Seq.hd
4.674 + |> (curry op COMP) (acc_downward
4.675 + |> (instantiate' [SOME (ctyp_of thy domT)]
4.676 + (map (SOME o cterm_of thy) [R, x, z]))
4.677 + |> forall_intr (cterm_of thy z)
4.678 + |> forall_intr (cterm_of thy x))
4.679 + |> forall_intr (cterm_of thy a)
4.680 + |> forall_intr (cterm_of thy P)
4.681 + in
4.682 + (subset_induct_all, simple_induct_rule)
4.683 + end
4.684 +
4.685 +
4.686 +
4.687 +(* FIXME: This should probably use fixed goals, to be more reliable and faster *)
4.688 +fun mk_domain_intro thy (Globals {domT, ...}) R R_cases clause =
4.689 + let
4.690 + val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
4.691 + qglr = (oqs, _, _, _), ...} = clause
4.692 + val goal = Trueprop (mk_acc domT R $ lhs)
4.693 + |> fold_rev (curry Logic.mk_implies) gs
4.694 + |> cterm_of thy
4.695 + in
4.696 + Goal.init goal
4.697 + |> (SINGLE (resolve_tac [accI] 1)) |> the
4.698 + |> (SINGLE (eresolve_tac [forall_elim_vars 0 R_cases] 1)) |> the
4.699 + |> (SINGLE (CLASIMPSET auto_tac)) |> the
4.700 + |> Goal.conclude
4.701 + |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
4.702 + end
4.703 +
4.704 +
4.705 +
4.706 +(** Termination rule **)
4.707 +
4.708 +val wf_induct_rule = thm "FunDef.wfP_induct_rule";
4.709 +val wf_in_rel = thm "FunDef.wf_in_rel";
4.710 +val in_rel_def = thm "FunDef.in_rel_def";
4.711 +
4.712 +fun mk_nest_term_case thy globals R' ihyp clause =
4.713 + let
4.714 + val Globals {x, z, ...} = globals
4.715 + val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
4.716 + qglr=(oqs, _, _, _), ...} = clause
4.717 +
4.718 + val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
4.719 +
4.720 + fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
4.721 + let
4.722 + val used = map (fn ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub)
4.723 +
4.724 + val hyp = Trueprop (R' $ arg $ lhs)
4.725 + |> fold_rev (curry Logic.mk_implies o prop_of) used
4.726 + |> FundefCtxTree.export_term (fixes, map prop_of assumes)
4.727 + |> fold_rev (curry Logic.mk_implies o prop_of) ags
4.728 + |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
4.729 + |> cterm_of thy
4.730 +
4.731 + val thm = assume hyp
4.732 + |> fold forall_elim cqs
4.733 + |> fold implies_elim_swp ags
4.734 + |> FundefCtxTree.import_thm thy (fixes, assumes) (* "(arg, lhs) : R'" *)
4.735 + |> fold implies_elim_swp used
4.736 +
4.737 + val acc = thm COMP ih_case
4.738 +
4.739 + val z_eq_arg = cterm_of thy (Trueprop (HOLogic.mk_eq (z, arg)))
4.740 +
4.741 + val arg_eq_z = (assume z_eq_arg) RS sym
4.742 +
4.743 + val z_acc = simplify (HOL_basic_ss addsimps [arg_eq_z]) acc (* fragile, slow... *)
4.744 + |> implies_intr (cprop_of case_hyp)
4.745 + |> implies_intr z_eq_arg
4.746 +
4.747 + val z_eq_arg = assume (cterm_of thy (Trueprop (mk_eq (z, arg))))
4.748 + val x_eq_lhs = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
4.749 +
4.750 + val ethm = (z_acc OF [z_eq_arg, x_eq_lhs])
4.751 + |> FundefCtxTree.export_thm thy (fixes,
4.752 + prop_of z_eq_arg :: prop_of x_eq_lhs :: map prop_of (ags @ assumes))
4.753 + |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
4.754 +
4.755 + val sub' = sub @ [(([],[]), acc)]
4.756 + in
4.757 + (sub', (hyp :: hyps, ethm :: thms))
4.758 + end
4.759 + | step _ _ _ _ = raise Match
4.760 + in
4.761 + FundefCtxTree.traverse_tree step tree
4.762 + end
4.763 +
4.764 +
4.765 +fun mk_nest_term_rule thy globals R R_cases clauses =
4.766 + let
4.767 + val Globals { domT, x, z, ... } = globals
4.768 + val acc_R = mk_acc domT R
4.769 +
4.770 + val R' = Free ("R", fastype_of R)
4.771 +
4.772 + val Rrel = Free ("R", mk_relT (domT, domT))
4.773 + val inrel_R = Const ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) $ Rrel
4.774 +
4.775 + val wfR' = cterm_of thy (Trueprop (Const ("FunDef.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
4.776 +
4.777 + (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
4.778 + val ihyp = all domT $ Abs ("z", domT,
4.779 + implies $ Trueprop (R' $ Bound 0 $ x)
4.780 + $ Trueprop (acc_R $ Bound 0))
4.781 + |> cterm_of thy
4.782 +
4.783 + val ihyp_a = assume ihyp |> forall_elim_vars 0
4.784 +
4.785 + val R_z_x = cterm_of thy (Trueprop (R $ z $ x))
4.786 +
4.787 + val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
4.788 + in
4.789 + R_cases
4.790 + |> forall_elim (cterm_of thy z)
4.791 + |> forall_elim (cterm_of thy x)
4.792 + |> forall_elim (cterm_of thy (acc_R $ z))
4.793 + |> curry op COMP (assume R_z_x)
4.794 + |> fold_rev (curry op COMP) cases
4.795 + |> implies_intr R_z_x
4.796 + |> forall_intr (cterm_of thy z)
4.797 + |> (fn it => it COMP accI)
4.798 + |> implies_intr ihyp
4.799 + |> forall_intr (cterm_of thy x)
4.800 + |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
4.801 + |> curry op RS (assume wfR')
4.802 + |> fold implies_intr hyps
4.803 + |> implies_intr wfR'
4.804 + |> forall_intr (cterm_of thy R')
4.805 + |> forall_elim (cterm_of thy (inrel_R))
4.806 + |> curry op RS wf_in_rel
4.807 + |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
4.808 + |> forall_intr (cterm_of thy Rrel)
4.809 + end
4.810 +
4.811 +
4.812 +
4.813 +(* Tail recursion (probably very fragile)
4.814 + *
4.815 + * FIXME:
4.816 + * - Need to do forall_elim_vars on psimps: Unneccesary, if psimps would be taken from the same context.
4.817 + * - Must we really replace the fvar by f here?
4.818 + * - Splitting is not configured automatically: Problems with case?
4.819 + *)
4.820 +fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps =
4.821 + let
4.822 + val Globals {domT, ranT, fvar, ...} = globals
4.823 +
4.824 + val R_cases = forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *)
4.825 +
4.826 + val graph_implies_dom = (* "G ?x ?y ==> dom ?x" *)
4.827 + Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
4.828 + (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))
4.829 + (fn {prems=[a], ...} =>
4.830 + ((rtac (G_induct OF [a]))
4.831 + THEN_ALL_NEW (rtac accI)
4.832 + THEN_ALL_NEW (etac R_cases)
4.833 + THEN_ALL_NEW (SIMPSET' asm_full_simp_tac)) 1)
4.834 +
4.835 + val default_thm = (forall_intr_vars graph_implies_dom) COMP (f_def COMP fundef_default_value)
4.836 +
4.837 + fun mk_trsimp clause psimp =
4.838 + let
4.839 + val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, qs, gs, lhs, rhs, ...}, ...} = clause
4.840 + val thy = ProofContext.theory_of ctxt
4.841 + val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
4.842 +
4.843 + val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
4.844 + val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
4.845 + in
4.846 + Goal.prove ctxt [] [] trsimp
4.847 + (fn _ =>
4.848 + rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
4.849 + THEN (rtac (forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
4.850 + THEN (SIMPSET (fn ss => asm_full_simp_tac (ss addsimps [default_thm]) 1))
4.851 + THEN (etac not_accP_down 1)
4.852 + THEN ((etac R_cases) THEN_ALL_NEW (SIMPSET' (fn ss => asm_full_simp_tac (ss addsimps [default_thm])))) 1)
4.853 + |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
4.854 + end
4.855 + in
4.856 + map2 mk_trsimp clauses psimps
4.857 + end
4.858 +
4.859 +
4.860 +fun prepare_fundef config defname (fname, fT, mixfix) abstract_qglrs default_str lthy =
4.861 + let
4.862 + val FundefConfig {domintros, tailrec, ...} = config
4.863 +
4.864 + val fvar = Free (fname, fT)
4.865 + val domT = domain_type fT
4.866 + val ranT = range_type fT
4.867 +
4.868 + val [default] = fst (Variable.importT_terms (fst (ProofContext.read_termTs lthy (K false) (K NONE) (K NONE) [] [(default_str, fT)])) lthy) (* FIXME *)
4.869 +
4.870 + val congs = get_fundef_congs (Context.Proof lthy)
4.871 + val (globals, ctxt') = fix_globals domT ranT fvar lthy
4.872 +
4.873 + val Globals { x, h, ... } = globals
4.874 +
4.875 + val clauses = map (mk_clause_context x ctxt') abstract_qglrs
4.876 +
4.877 + val n = length abstract_qglrs
4.878 +
4.879 + val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs) (* FIXME: Save in theory *)
4.880 +
4.881 + fun build_tree (ClauseContext { ctxt, rhs, ...}) =
4.882 + FundefCtxTree.mk_tree congs_deps (fname, fT) h ctxt rhs
4.883 +
4.884 + val trees = map build_tree clauses
4.885 + val RCss = map find_calls trees
4.886 +
4.887 + val ((G, GIntro_thms, G_elim, G_induct), lthy) =
4.888 + PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
4.889 +
4.890 + val ((f, f_defthm), lthy) =
4.891 + PROFILE "def_fun" (define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default) lthy
4.892 +
4.893 + val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
4.894 + val trees = map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
4.895 +
4.896 + val ((R, RIntro_thmss, R_elim), lthy) =
4.897 + PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
4.898 +
4.899 + val (_, lthy) =
4.900 + LocalTheory.abbrev Syntax.default_mode ((defname ^ "_dom", NoSyn), mk_acc domT R) lthy
4.901 +
4.902 + val newthy = ProofContext.theory_of lthy
4.903 + val clauses = map (transfer_clause_ctx newthy) clauses
4.904 +
4.905 + val cert = cterm_of (ProofContext.theory_of lthy)
4.906 +
4.907 + val xclauses = PROFILE "xclauses" (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss
4.908 +
4.909 + val complete = mk_completeness globals clauses abstract_qglrs |> cert |> assume
4.910 + val compat = mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> assume)
4.911 +
4.912 + val compat_store = store_compat_thms n compat
4.913 +
4.914 + val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff newthy congs globals G f R xclauses complete compat compat_store G_elim) f_defthm
4.915 +
4.916 + val mk_trsimps = mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses
4.917 +
4.918 + fun mk_partial_rules provedgoal =
4.919 + let
4.920 + val newthy = theory_of_thm provedgoal (*FIXME*)
4.921 +
4.922 + val (graph_is_function, complete_thm) =
4.923 + provedgoal
4.924 + |> Conjunction.elim
4.925 + |> apfst (forall_elim_vars 0)
4.926 +
4.927 + val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
4.928 +
4.929 + val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
4.930 +
4.931 + val (subset_pinduct, simple_pinduct) = PROFILE "Proving partial induction rule"
4.932 + (mk_partial_induct_rule newthy globals R complete_thm) xclauses
4.933 +
4.934 +
4.935 + val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses
4.936 +
4.937 + val dom_intros = if domintros
4.938 + then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro newthy globals R R_elim)) xclauses)
4.939 + else NONE
4.940 + val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
4.941 +
4.942 + in
4.943 + FundefResult {f=f, G=G, R=R, cases=complete_thm,
4.944 + psimps=psimps, subset_pinducts=[subset_pinduct], simple_pinducts=[simple_pinduct],
4.945 + termination=total_intro, trsimps=trsimps,
4.946 + domintros=dom_intros}
4.947 + end
4.948 + in
4.949 + ((f, goalstate, mk_partial_rules), lthy)
4.950 + end
4.951 +
4.952 +
4.953 +
4.954 +
4.955 +end
5.1 --- a/src/HOL/Tools/function_package/fundef_lib.ML Mon Jan 22 16:53:33 2007 +0100
5.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML Mon Jan 22 17:29:43 2007 +0100
5.3 @@ -10,14 +10,34 @@
5.4
5.5 structure FundefLib = struct
5.6
5.7 +(* ==> library/string *)
5.8 fun plural sg pl [x] = sg
5.9 | plural sg pl _ = pl
5.10
5.11 +
5.12 +
5.13 +fun map_option f NONE = NONE
5.14 + | map_option f (SOME x) = SOME (f x);
5.15 +
5.16 +fun fold_option f NONE y = y
5.17 + | fold_option f (SOME x) y = f x y;
5.18 +
5.19 +fun fold_map_option f NONE y = (NONE, y)
5.20 + | fold_map_option f (SOME x) y = apfst SOME (f x y);
5.21 +
5.22 +
5.23 +
5.24 +
5.25 +
5.26 +
5.27 +(* ??? *)
5.28 fun eq_str (s : string, t) = (s = t) (* monomorphic equality on strings *)
5.29
5.30 +(* ==> logic.ML? *)
5.31 fun mk_forall v t = all (fastype_of v) $ lambda v t
5.32
5.33 -(* Constructs a tupled abstraction from an arbitrarily nested tuple of variables and a term. *)
5.34 +(* lambda-abstracts over an arbitrarily nested tuple
5.35 + ==> hologic.ML? *)
5.36 fun tupled_lambda vars t =
5.37 case vars of
5.38 (Free v) => lambda (Free v) t
5.39 @@ -86,16 +106,12 @@
5.40
5.41
5.42 (* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *)
5.43 +(* ==> library *)
5.44 fun unordered_pairs [] = []
5.45 | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs
5.46
5.47
5.48 -(* Replaces Frees by name. Probably quicker than Pattern.rewrite_terms, and works with loose Bounds. *)
5.49 -fun replace_frees assoc =
5.50 - map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n)
5.51 - | t => t)
5.52 -
5.53 -
5.54 +(* term.ML *)
5.55 fun forall_aterms P (t $ u) = forall_aterms P t andalso forall_aterms P u
5.56 | forall_aterms P (Abs (_, _, t)) = forall_aterms P t
5.57 | forall_aterms P a = P a
5.58 @@ -104,6 +120,11 @@
5.59
5.60
5.61
5.62 +(* Replaces Frees by name. Probably quicker than Pattern.rewrite_terms, and works with loose Bounds. *)
5.63 +fun replace_frees assoc =
5.64 + map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n)
5.65 + | t => t)
5.66 +
5.67
5.68 fun rename_bound n (Q $ Abs(_, T, b)) = (Q $ Abs(n, T, b))
5.69 | rename_bound n _ = raise Match
5.70 @@ -116,7 +137,7 @@
5.71 fun forall_intr_rename (n, cv) thm =
5.72 let
5.73 val allthm = forall_intr cv thm
5.74 - val (_, abs) = Logic.dest_all (prop_of allthm)
5.75 + val (_ $ abs) = prop_of allthm
5.76 in
5.77 Thm.rename_boundvars abs (Abs (n, dummyT, dummy_term)) allthm
5.78 end
5.79 @@ -127,11 +148,6 @@
5.80 Term.add_frees t []
5.81 |> filter_out (Variable.is_fixed ctxt o fst)
5.82 |> rev
5.83 -(*
5.84 - rev (fold_aterms (fn Free (v as (x, _)) =>
5.85 - if Variable.is_fixed ctxt x then I else insert (fn ((x, _),(y, _)) => x = y) v | _ => I) t [])
5.86 -*)
5.87 -
5.88
5.89
5.90 end
6.1 --- a/src/HOL/Tools/function_package/fundef_package.ML Mon Jan 22 16:53:33 2007 +0100
6.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML Mon Jan 22 17:29:43 2007 +0100
6.3 @@ -40,6 +40,8 @@
6.4
6.5 val note_theorem = LocalTheory.note Thm.theoremK
6.6
6.7 +fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
6.8 +
6.9 fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *)
6.10 let val (xs, ys) = split_list ps
6.11 in xs ~~ f ys end
6.12 @@ -47,49 +49,46 @@
6.13 fun restore_spec_structure reps spec =
6.14 (burrow o burrow_snd o burrow o K) reps spec
6.15
6.16 -fun add_simps label moreatts mutual_info fixes psimps spec lthy =
6.17 +fun add_simps fixes spec sort label moreatts simps lthy =
6.18 let
6.19 val fnames = map (fst o fst) fixes
6.20
6.21 - val (saved_spec_psimps, lthy) =
6.22 - fold_map (fold_map note_theorem) (restore_spec_structure psimps spec) lthy
6.23 - val saved_psimps = flat (map snd (flat saved_spec_psimps))
6.24 + val (saved_spec_simps, lthy) =
6.25 + fold_map (fold_map note_theorem) (restore_spec_structure simps spec) lthy
6.26 + val saved_simps = flat (map snd (flat saved_spec_simps))
6.27
6.28 - val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames saved_psimps
6.29 + val simps_by_f = sort saved_simps
6.30
6.31 - fun add_for_f fname psimps =
6.32 + fun add_for_f fname simps =
6.33 note_theorem
6.34 ((NameSpace.qualified fname label, Attrib.internal (K Simplifier.simp_add) :: moreatts),
6.35 - psimps) #> snd
6.36 + simps) #> snd
6.37 in
6.38 - (saved_psimps,
6.39 - fold2 add_for_f fnames psimps_by_f lthy)
6.40 + (saved_simps,
6.41 + fold2 add_for_f fnames simps_by_f lthy)
6.42 end
6.43
6.44
6.45 -fun fundef_afterqed config fixes spec mutual_info defname data [[result]] lthy =
6.46 +fun fundef_afterqed config fixes spec defname cont sort_cont [[proof]] lthy =
6.47 let
6.48 - val FundefConfig { domintros, ...} = config
6.49 - val Prep {f, R, ...} = data
6.50 - val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result
6.51 - val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
6.52 + val FundefResult {f, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} =
6.53 + cont (Goal.close_result proof)
6.54 +
6.55 val qualify = NameSpace.qualified defname
6.56 + val addsimps = add_simps fixes spec sort_cont
6.57
6.58 val (((psimps', pinducts'), (_, [termination'])), lthy) =
6.59 lthy
6.60 - |> PROFILE "adding_psimps" (add_simps "psimps" [] mutual_info fixes psimps spec)
6.61 - ||>> PROFILE "adding pinduct"
6.62 - (note_theorem ((qualify "pinduct",
6.63 - [Attrib.internal (K (InductAttrib.induct_set ""))]), simple_pinducts))
6.64 - ||>> PROFILE "adding termination"
6.65 - (note_theorem ((qualify "termination", []), [termination]))
6.66 - ||> (snd o PROFILE "adding cases" (note_theorem ((qualify "cases", []), [cases])))
6.67 - ||> (snd o PROFILE "adding domintros" (note_theorem ((qualify "domintros", []), domintros)))
6.68 + |> addsimps "psimps" [] psimps
6.69 + ||> fold_option (snd oo addsimps "simps" []) trsimps
6.70 + ||>> note_theorem ((qualify "pinduct",
6.71 + [Attrib.internal (K (InductAttrib.induct_set ""))]), simple_pinducts)
6.72 + ||>> note_theorem ((qualify "termination", []), [termination])
6.73 + ||> (snd o note_theorem ((qualify "cases", []), [cases]))
6.74 + ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
6.75
6.76 - val cdata = FundefCtxData { fixes=fixes, spec=spec, mutual=mutual_info, psimps=psimps',
6.77 + val cdata = FundefCtxData { add_simps=addsimps, psimps=psimps',
6.78 pinducts=snd pinducts', termination=termination', f=f, R=R }
6.79 -
6.80 -
6.81 in
6.82 lthy (* FIXME proper handling of morphism *)
6.83 |> LocalTheory.declaration (fn phi => add_fundef_data defname cdata) (* save in target *)
6.84 @@ -117,33 +116,36 @@
6.85
6.86 fun gen_add_fundef prep_spec fixspec eqnss_flags config lthy =
6.87 let
6.88 - val FundefConfig {sequential, default, ...} = config
6.89 + val FundefConfig {sequential, default, tailrec, ...} = config
6.90
6.91 val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags sequential lthy
6.92 +
6.93 + val defname = mk_defname fixes
6.94 +
6.95 val t_eqns = spec
6.96 |> flat |> map snd |> flat (* flatten external structure *)
6.97
6.98 - val ((mutual_info, name, prep_result as Prep {goal, goalI, ...}), lthy) =
6.99 - FundefMutual.prepare_fundef_mutual fixes t_eqns default lthy
6.100 + val ((goalstate, cont, sort_cont), lthy) =
6.101 + FundefMutual.prepare_fundef_mutual config defname fixes t_eqns default lthy
6.102
6.103 - val afterqed = fundef_afterqed config fixes spec mutual_info name prep_result
6.104 + val afterqed = fundef_afterqed config fixes spec defname cont sort_cont
6.105 in
6.106 - (name, lthy
6.107 - |> Proof.theorem_i NONE afterqed [[(goal, [])]]
6.108 - |> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd)
6.109 + (defname, lthy
6.110 + |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
6.111 + |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd)
6.112 end
6.113
6.114
6.115 fun total_termination_afterqed defname data [[totality]] lthy =
6.116 let
6.117 - val FundefCtxData { fixes, spec, mutual, psimps, pinducts, ... } = data
6.118 + val FundefCtxData { add_simps, psimps, pinducts, ... } = data
6.119
6.120 - val totality = PROFILE "closing" Goal.close_result totality
6.121 + val totality = Goal.close_result totality
6.122
6.123 val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
6.124
6.125 - val tsimps = PROFILE "making tsimps" (map remove_domain_condition) psimps
6.126 - val tinduct = PROFILE "making tinduct" (map remove_domain_condition) pinducts
6.127 + val tsimps = map remove_domain_condition psimps
6.128 + val tinduct = map remove_domain_condition pinducts
6.129
6.130 (* FIXME: How to generate code from (possibly) local contexts*)
6.131 val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
6.132 @@ -152,26 +154,26 @@
6.133 val qualify = NameSpace.qualified defname;
6.134 in
6.135 lthy
6.136 - |> PROFILE "adding tsimps" (add_simps "simps" allatts mutual fixes tsimps spec) |> snd
6.137 - |> PROFILE "adding tinduct" (note_theorem ((qualify "induct", []), tinduct)) |> snd
6.138 + |> add_simps "simps" allatts tsimps |> snd
6.139 + |> note_theorem ((qualify "induct", []), tinduct) |> snd
6.140 end
6.141
6.142
6.143 fun setup_termination_proof name_opt lthy =
6.144 let
6.145 - val name = the_default (get_last_fundef (Context.Proof lthy)) name_opt
6.146 - val data = the (get_fundef_data name (Context.Proof lthy))
6.147 - handle Option.Option => raise ERROR ("No such function definition: " ^ name)
6.148 + val defname = the_default (get_last_fundef (Context.Proof lthy)) name_opt
6.149 + val data = the (get_fundef_data defname (Context.Proof lthy))
6.150 + handle Option.Option => raise ERROR ("No such function definition: " ^ defname)
6.151
6.152 - val FundefCtxData {termination, f, R, ...} = data
6.153 - val goal = FundefTermination.mk_total_termination_goal f R
6.154 + val FundefCtxData {termination, R, ...} = data
6.155 + val goal = FundefTermination.mk_total_termination_goal R
6.156 in
6.157 lthy
6.158 |> ProofContext.note_thmss_i ""
6.159 [(("termination", [ContextRules.intro_query NONE]),
6.160 [([Goal.norm_result termination], [])])] |> snd
6.161 |> set_termination_rule termination
6.162 - |> Proof.theorem_i NONE (total_termination_afterqed name data) [[(goal, [])]]
6.163 + |> Proof.theorem_i NONE (total_termination_afterqed defname data) [[(goal, [])]]
6.164 end
6.165
6.166
7.1 --- a/src/HOL/Tools/function_package/fundef_prep.ML Mon Jan 22 16:53:33 2007 +0100
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,534 +0,0 @@
7.4 -(* Title: HOL/Tools/function_package/fundef_prep.ML
7.5 - ID: $Id$
7.6 - Author: Alexander Krauss, TU Muenchen
7.7 -
7.8 -A package for general recursive function definitions.
7.9 -Preparation step: makes auxiliary definitions and generates
7.10 -proof obligations.
7.11 -*)
7.12 -
7.13 -signature FUNDEF_PREP =
7.14 -sig
7.15 - val prepare_fundef : string (* defname *)
7.16 - -> (string * typ * mixfix) (* defined symbol *)
7.17 - -> ((string * typ) list * term list * term * term) list (* specification *)
7.18 - -> string (* default_value, not parsed yet *)
7.19 - -> local_theory
7.20 - -> FundefCommon.prep_result * term * local_theory
7.21 -
7.22 -end
7.23 -
7.24 -structure FundefPrep : FUNDEF_PREP =
7.25 -struct
7.26 -
7.27 -
7.28 -open FundefLib
7.29 -open FundefCommon
7.30 -open FundefAbbrev
7.31 -
7.32 -(* Theory dependencies. *)
7.33 -val Pair_inject = thm "Product_Type.Pair_inject";
7.34 -
7.35 -val acc_induct_rule = thm "FunDef.accP_induct_rule"
7.36 -
7.37 -val ex1_implies_ex = thm "FunDef.fundef_ex1_existence"
7.38 -val ex1_implies_un = thm "FunDef.fundef_ex1_uniqueness"
7.39 -val ex1_implies_iff = thm "FunDef.fundef_ex1_iff"
7.40 -
7.41 -val conjunctionI = thm "conjunctionI";
7.42 -
7.43 -
7.44 -
7.45 -fun find_calls tree =
7.46 - let
7.47 - fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs)
7.48 - | add_Ri _ _ _ _ = raise Match
7.49 - in
7.50 - rev (FundefCtxTree.traverse_tree add_Ri tree [])
7.51 - end
7.52 -
7.53 -
7.54 -fun mk_compat_proof_obligations domT ranT fvar f glrs =
7.55 - let
7.56 - fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
7.57 - let
7.58 - val shift = incr_boundvars (length qs')
7.59 - in
7.60 - (implies $ Trueprop (eq_const domT $ shift lhs $ lhs')
7.61 - $ Trueprop (eq_const ranT $ shift rhs $ rhs'))
7.62 - |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
7.63 - |> fold_rev (fn (n,T) => fn b => all T $ Abs(n,T,b)) (qs @ qs')
7.64 - |> curry abstract_over fvar
7.65 - |> curry subst_bound f
7.66 - end
7.67 - in
7.68 - map mk_impl (unordered_pairs glrs)
7.69 - end
7.70 -
7.71 -
7.72 -fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
7.73 - let
7.74 - fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
7.75 - Trueprop Pbool
7.76 - |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
7.77 - |> fold_rev (curry Logic.mk_implies) gs
7.78 - |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
7.79 - in
7.80 - Trueprop Pbool
7.81 - |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
7.82 - |> mk_forall_rename ("x", x)
7.83 - |> mk_forall_rename ("P", Pbool)
7.84 - end
7.85 -
7.86 -
7.87 -fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
7.88 - let
7.89 - val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
7.90 - |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
7.91 -
7.92 - val thy = ProofContext.theory_of ctxt'
7.93 -
7.94 - fun inst t = subst_bounds (rev qs, t)
7.95 - val gs = map inst pre_gs
7.96 - val lhs = inst pre_lhs
7.97 - val rhs = inst pre_rhs
7.98 -
7.99 - val cqs = map (cterm_of thy) qs
7.100 - val ags = map (assume o cterm_of thy) gs
7.101 -
7.102 - val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
7.103 - in
7.104 - ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
7.105 - cqs = cqs, ags = ags, case_hyp = case_hyp }
7.106 - end
7.107 -
7.108 -
7.109 -(* lowlevel term function *)
7.110 -fun abstract_over_list vs body =
7.111 - let
7.112 - exception SAME;
7.113 - fun abs lev v tm =
7.114 - if v aconv tm then Bound lev
7.115 - else
7.116 - (case tm of
7.117 - Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
7.118 - | t $ u => (abs lev v t $ (abs lev v u handle SAME => u) handle SAME => t $ abs lev v u)
7.119 - | _ => raise SAME);
7.120 - in
7.121 - fold_index (fn (i,v) => fn t => abs i v t handle SAME => t) vs body
7.122 - end
7.123 -
7.124 -
7.125 -
7.126 -fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
7.127 - let
7.128 - val Globals {h, fvar, x, ...} = globals
7.129 -
7.130 - val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
7.131 - val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
7.132 -
7.133 - (* Instantiate the GIntro thm with "f" and import into the clause context. *)
7.134 - val lGI = GIntro_thm
7.135 - |> forall_elim (cert f)
7.136 - |> fold forall_elim cqs
7.137 - |> fold implies_elim_swp ags
7.138 -
7.139 - fun mk_call_info (rcfix, rcassm, rcarg) RI =
7.140 - let
7.141 - val llRI = RI
7.142 - |> fold forall_elim cqs
7.143 - |> fold (forall_elim o cert o Free) rcfix
7.144 - |> fold implies_elim_swp ags
7.145 - |> fold implies_elim_swp rcassm
7.146 -
7.147 - val h_assum =
7.148 - Trueprop (G $ rcarg $ (h $ rcarg))
7.149 - |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
7.150 - |> fold_rev (mk_forall o Free) rcfix
7.151 - |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
7.152 - |> abstract_over_list (rev qs)
7.153 - in
7.154 - RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
7.155 - end
7.156 -
7.157 - val RC_infos = map2 mk_call_info RCs RIntro_thms
7.158 - in
7.159 - ClauseInfo
7.160 - {
7.161 - no=no,
7.162 - cdata=cdata,
7.163 - qglr=qglr,
7.164 -
7.165 - lGI=lGI,
7.166 - RCs=RC_infos,
7.167 - tree=tree
7.168 - }
7.169 - end
7.170 -
7.171 -
7.172 -
7.173 -
7.174 -
7.175 -
7.176 -
7.177 -(* replace this by a table later*)
7.178 -fun store_compat_thms 0 thms = []
7.179 - | store_compat_thms n thms =
7.180 - let
7.181 - val (thms1, thms2) = chop n thms
7.182 - in
7.183 - (thms1 :: store_compat_thms (n - 1) thms2)
7.184 - end
7.185 -
7.186 -(* expects i <= j *)
7.187 -fun lookup_compat_thm i j cts =
7.188 - nth (nth cts (i - 1)) (j - i)
7.189 -
7.190 -(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
7.191 -(* if j < i, then turn around *)
7.192 -fun get_compat_thm thy cts i j ctxi ctxj =
7.193 - let
7.194 - val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
7.195 - val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
7.196 -
7.197 - val lhsi_eq_lhsj = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj)))
7.198 - in if j < i then
7.199 - let
7.200 - val compat = lookup_compat_thm j i cts
7.201 - in
7.202 - compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
7.203 - |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
7.204 - |> fold implies_elim_swp agsj
7.205 - |> fold implies_elim_swp agsi
7.206 - |> implies_elim_swp ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
7.207 - end
7.208 - else
7.209 - let
7.210 - val compat = lookup_compat_thm i j cts
7.211 - in
7.212 - compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
7.213 - |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
7.214 - |> fold implies_elim_swp agsi
7.215 - |> fold implies_elim_swp agsj
7.216 - |> implies_elim_swp (assume lhsi_eq_lhsj)
7.217 - |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
7.218 - end
7.219 - end
7.220 -
7.221 -
7.222 -
7.223 -
7.224 -(* Generates the replacement lemma in fully quantified form. *)
7.225 -fun mk_replacement_lemma thy h ih_elim clause =
7.226 - let
7.227 - val ClauseInfo {cdata=ClauseContext {qs, lhs, rhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
7.228 -
7.229 - val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
7.230 -
7.231 - val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
7.232 - val h_assums = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
7.233 -
7.234 - val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
7.235 -
7.236 - val (eql, _) = FundefCtxTree.rewrite_by_tree thy h ih_elim_case_inst (Ris ~~ h_assums) tree
7.237 -
7.238 - val replace_lemma = (eql RS meta_eq_to_obj_eq)
7.239 - |> implies_intr (cprop_of case_hyp)
7.240 - |> fold_rev (implies_intr o cprop_of) h_assums
7.241 - |> fold_rev (implies_intr o cprop_of) ags
7.242 - |> fold_rev forall_intr cqs
7.243 - |> Goal.close_result
7.244 - in
7.245 - replace_lemma
7.246 - end
7.247 -
7.248 -
7.249 -fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj =
7.250 - let
7.251 - val Globals {h, y, x, fvar, ...} = globals
7.252 - val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
7.253 - val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
7.254 -
7.255 - val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...}
7.256 - = mk_clause_context x ctxti cdescj
7.257 -
7.258 - val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
7.259 - val compat = get_compat_thm thy compat_store i j cctxi cctxj
7.260 - val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
7.261 -
7.262 - val RLj_import =
7.263 - RLj |> fold forall_elim cqsj'
7.264 - |> fold implies_elim_swp agsj'
7.265 - |> fold implies_elim_swp Ghsj'
7.266 -
7.267 - val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
7.268 - val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
7.269 - in
7.270 - (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
7.271 - |> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
7.272 - |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
7.273 - |> (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.274 - |> fold_rev (implies_intr o cprop_of) Ghsj'
7.275 - |> fold_rev (implies_intr o cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
7.276 - |> implies_intr (cprop_of y_eq_rhsj'h)
7.277 - |> implies_intr (cprop_of lhsi_eq_lhsj')
7.278 - |> fold_rev forall_intr (cterm_of thy h :: cqsj')
7.279 - end
7.280 -
7.281 -
7.282 -
7.283 -fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
7.284 - let
7.285 - val Globals {x, y, ranT, fvar, ...} = globals
7.286 - val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
7.287 - val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
7.288 -
7.289 - val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
7.290 -
7.291 - fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
7.292 - |> fold_rev (implies_intr o cprop_of) CCas
7.293 - |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
7.294 -
7.295 - val existence = fold (curry op COMP o prep_RC) RCs lGI
7.296 -
7.297 - val P = cterm_of thy (mk_eq (y, rhsC))
7.298 - val G_lhs_y = assume (cterm_of thy (Trueprop (G $ lhs $ y)))
7.299 -
7.300 - val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas
7.301 -
7.302 - val uniqueness = G_cases
7.303 - |> forall_elim (cterm_of thy lhs)
7.304 - |> forall_elim (cterm_of thy y)
7.305 - |> forall_elim P
7.306 - |> implies_elim_swp G_lhs_y
7.307 - |> fold implies_elim_swp unique_clauses
7.308 - |> implies_intr (cprop_of G_lhs_y)
7.309 - |> forall_intr (cterm_of thy y)
7.310 -
7.311 - val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
7.312 -
7.313 - val exactly_one =
7.314 - ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
7.315 - |> curry (op COMP) existence
7.316 - |> curry (op COMP) uniqueness
7.317 - |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
7.318 - |> implies_intr (cprop_of case_hyp)
7.319 - |> fold_rev (implies_intr o cprop_of) ags
7.320 - |> fold_rev forall_intr cqs
7.321 -
7.322 - val function_value =
7.323 - existence
7.324 - |> implies_intr ihyp
7.325 - |> implies_intr (cprop_of case_hyp)
7.326 - |> forall_intr (cterm_of thy x)
7.327 - |> forall_elim (cterm_of thy lhs)
7.328 - |> curry (op RS) refl
7.329 - in
7.330 - (exactly_one, function_value)
7.331 - end
7.332 -
7.333 -
7.334 -
7.335 -
7.336 -fun prove_stuff thy congs globals G f R clauses complete compat compat_store G_elim f_def =
7.337 - let
7.338 - val Globals {h, domT, ranT, x, ...} = globals
7.339 -
7.340 - val inst_ex1_ex = f_def RS ex1_implies_ex
7.341 - val inst_ex1_un = f_def RS ex1_implies_un
7.342 - val inst_ex1_iff = f_def RS ex1_implies_iff
7.343 -
7.344 - (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
7.345 - val ihyp = all domT $ Abs ("z", domT,
7.346 - implies $ Trueprop (R $ Bound 0 $ x)
7.347 - $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
7.348 - Abs ("y", ranT, G $ Bound 1 $ Bound 0)))
7.349 - |> cterm_of thy
7.350 -
7.351 - val ihyp_thm = assume ihyp |> forall_elim_vars 0
7.352 - val ih_intro = ihyp_thm RS inst_ex1_ex
7.353 - val ih_elim = ihyp_thm RS inst_ex1_un
7.354 -
7.355 - val _ = Output.debug (fn () => "Proving Replacement lemmas...")
7.356 - val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
7.357 -
7.358 - val _ = Output.debug (fn () => "Proving cases for unique existence...")
7.359 - val (ex1s, values) =
7.360 - split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
7.361 -
7.362 - val _ = Output.debug (fn () => "Proving: Graph is a function") (* FIXME: Rewrite this proof. *)
7.363 - val graph_is_function = complete
7.364 - |> forall_elim_vars 0
7.365 - |> fold (curry op COMP) ex1s
7.366 - |> implies_intr (ihyp)
7.367 - |> implies_intr (cterm_of thy (Trueprop (mk_acc domT R $ x)))
7.368 - |> forall_intr (cterm_of thy x)
7.369 - |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
7.370 - |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
7.371 -
7.372 - val goal = complete COMP (graph_is_function COMP conjunctionI)
7.373 - |> Goal.close_result
7.374 -
7.375 - val goalI = Goal.protect goal
7.376 - |> fold_rev (implies_intr o cprop_of) compat
7.377 - |> implies_intr (cprop_of complete)
7.378 - in
7.379 - (prop_of goal, goalI, inst_ex1_iff, values)
7.380 - end
7.381 -
7.382 -
7.383 -fun define_graph Gname fvar domT ranT clauses RCss lthy =
7.384 - let
7.385 - val GT = domT --> ranT --> boolT
7.386 - val Gvar = Free (the_single (Variable.variant_frees lthy [] [(Gname, GT)]))
7.387 -
7.388 - fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
7.389 - let
7.390 - fun mk_h_assm (rcfix, rcassm, rcarg) =
7.391 - Trueprop (Gvar $ rcarg $ (fvar $ rcarg))
7.392 - |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
7.393 - |> fold_rev (mk_forall o Free) rcfix
7.394 - in
7.395 - Trueprop (Gvar $ lhs $ rhs)
7.396 - |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
7.397 - |> fold_rev (curry Logic.mk_implies) gs
7.398 - |> fold_rev mk_forall (fvar :: qs)
7.399 - end
7.400 -
7.401 - val G_intros = map2 mk_GIntro clauses RCss
7.402 -
7.403 - val (GIntro_thms, (G, G_elim, lthy)) =
7.404 - FundefInductiveWrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy)
7.405 - in
7.406 - ((G, GIntro_thms, G_elim), lthy)
7.407 - end
7.408 -
7.409 -
7.410 -
7.411 -fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
7.412 - let
7.413 - val f_def =
7.414 - Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
7.415 - Abs ("y", ranT, G $ Bound 1 $ Bound 0))
7.416 - |> Envir.beta_norm (* FIXME: LocalTheory.def does not work if not beta-normal *)
7.417 -
7.418 - val ((f, (_, f_defthm)), lthy) =
7.419 - LocalTheory.def Thm.internalK ((fname ^ "C", mixfix), ((fdefname, []), f_def)) lthy
7.420 - in
7.421 - ((f, f_defthm), lthy)
7.422 - end
7.423 -
7.424 -
7.425 -fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy =
7.426 - let
7.427 -
7.428 - val RT = domT --> domT --> boolT
7.429 - val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)]))
7.430 -
7.431 - fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
7.432 - Trueprop (Rvar $ rcarg $ lhs)
7.433 - |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
7.434 - |> fold_rev (curry Logic.mk_implies) gs
7.435 - |> fold_rev (mk_forall o Free) rcfix
7.436 - |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
7.437 - (* "!!qs xs. CS ==> G => (r, lhs) : R" *)
7.438 -
7.439 - val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
7.440 -
7.441 - val (RIntro_thmss, (R, R_elim, lthy)) =
7.442 - fold_burrow FundefInductiveWrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy)
7.443 - in
7.444 - ((R, RIntro_thmss, R_elim), lthy)
7.445 - end
7.446 -
7.447 -
7.448 -fun fix_globals domT ranT fvar ctxt =
7.449 - let
7.450 - val ([h, y, x, z, a, D, P, Pbool],ctxt') =
7.451 - Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
7.452 - in
7.453 - (Globals {h = Free (h, domT --> ranT),
7.454 - y = Free (y, ranT),
7.455 - x = Free (x, domT),
7.456 - z = Free (z, domT),
7.457 - a = Free (a, domT),
7.458 - D = Free (D, domT --> boolT),
7.459 - P = Free (P, domT --> boolT),
7.460 - Pbool = Free (Pbool, boolT),
7.461 - fvar = fvar,
7.462 - domT = domT,
7.463 - ranT = ranT
7.464 - },
7.465 - ctxt')
7.466 - end
7.467 -
7.468 -
7.469 -
7.470 -fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
7.471 - let
7.472 - fun inst_term t = subst_bound(f, abstract_over (fvar, t))
7.473 - in
7.474 - (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
7.475 - end
7.476 -
7.477 -
7.478 -
7.479 -fun prepare_fundef defname (fname, fT, mixfix) abstract_qglrs default_str lthy =
7.480 - let
7.481 - val fvar = Free (fname, fT)
7.482 - val domT = domain_type fT
7.483 - val ranT = range_type fT
7.484 -
7.485 - val [default] = fst (Variable.importT_terms (fst (ProofContext.read_termTs lthy (K false) (K NONE) (K NONE) [] [(default_str, fT)])) lthy) (* FIXME *)
7.486 -
7.487 - val congs = get_fundef_congs (Context.Proof lthy)
7.488 - val (globals, ctxt') = fix_globals domT ranT fvar lthy
7.489 -
7.490 - val Globals { x, h, ... } = globals
7.491 -
7.492 - val clauses = PROFILE "mk_clause_context" (map (mk_clause_context x ctxt')) abstract_qglrs
7.493 -
7.494 - val n = length abstract_qglrs
7.495 -
7.496 - val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs) (* FIXME: Save in theory *)
7.497 -
7.498 - fun build_tree (ClauseContext { ctxt, rhs, ...}) =
7.499 - FundefCtxTree.mk_tree congs_deps (fname, fT) h ctxt rhs
7.500 -
7.501 - val trees = PROFILE "making trees" (map build_tree) clauses
7.502 - val RCss = PROFILE "finding calls" (map find_calls) trees
7.503 -
7.504 - val ((G, GIntro_thms, G_elim), lthy) = PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
7.505 - val ((f, f_defthm), lthy) = PROFILE "def_fun" (define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default) lthy
7.506 -
7.507 - val RCss = PROFILE "inst_RCs" (map (map (inst_RC (ProofContext.theory_of lthy) fvar f))) RCss
7.508 - val trees = PROFILE "inst_trees" (map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f)) trees
7.509 -
7.510 - val ((R, RIntro_thmss, R_elim), lthy) =
7.511 - PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
7.512 -
7.513 - val (_, lthy) = PROFILE "abbrev"
7.514 - (LocalTheory.abbrev Syntax.default_mode ((defname ^ "_dom", NoSyn), mk_acc domT R)) lthy
7.515 -
7.516 - val newthy = ProofContext.theory_of lthy
7.517 - val clauses = map (transfer_clause_ctx newthy) clauses
7.518 -
7.519 - val cert = cterm_of (ProofContext.theory_of lthy)
7.520 -
7.521 - val xclauses = PROFILE "xclauses" (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss
7.522 -
7.523 - val complete = PROFILE "mk_compl" (mk_completeness globals clauses) abstract_qglrs |> cert |> assume
7.524 - val compat = PROFILE "mk_compat" (mk_compat_proof_obligations domT ranT fvar f) abstract_qglrs |> map (cert #> assume)
7.525 -
7.526 - val compat_store = store_compat_thms n compat
7.527 -
7.528 - val (goal, goalI, ex1_iff, values) = PROFILE "prove_stuff" (prove_stuff newthy congs globals G f R xclauses complete compat compat_store G_elim) f_defthm
7.529 - in
7.530 - (Prep {globals = globals, f = f, G = G, R = R, goal = goal, goalI = goalI, values = values, clauses = xclauses, ex1_iff = ex1_iff, R_cases = R_elim}, f,
7.531 - lthy)
7.532 - end
7.533 -
7.534 -
7.535 -
7.536 -
7.537 -end
8.1 --- a/src/HOL/Tools/function_package/fundef_proof.ML Mon Jan 22 16:53:33 2007 +0100
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,327 +0,0 @@
8.4 -(* Title: HOL/Tools/function_package/fundef_proof.ML
8.5 - ID: $Id$
8.6 - Author: Alexander Krauss, TU Muenchen
8.7 -
8.8 -A package for general recursive function definitions.
8.9 -Internal proofs.
8.10 -*)
8.11 -
8.12 -
8.13 -signature FUNDEF_PROOF =
8.14 -sig
8.15 -
8.16 - val mk_partial_rules : theory -> FundefCommon.prep_result
8.17 - -> thm -> FundefCommon.fundef_result
8.18 -end
8.19 -
8.20 -
8.21 -structure FundefProof : FUNDEF_PROOF =
8.22 -struct
8.23 -
8.24 -open FundefLib
8.25 -open FundefCommon
8.26 -open FundefAbbrev
8.27 -
8.28 -(* Theory dependencies *)
8.29 -val subsetD = thm "subsetD"
8.30 -val split_apply = thm "Product_Type.split"
8.31 -val wf_induct_rule = thm "FunDef.wfP_induct_rule";
8.32 -val Pair_inject = thm "Product_Type.Pair_inject";
8.33 -
8.34 -val wf_in_rel = thm "FunDef.wf_in_rel";
8.35 -val in_rel_def = thm "FunDef.in_rel_def";
8.36 -
8.37 -val acc_induct_rule = thm "FunDef.accP_induct_rule"
8.38 -val acc_downward = thm "FunDef.accP_downward"
8.39 -val accI = thm "FunDef.accPI"
8.40 -
8.41 -val acc_subset_induct = thm "FunDef.accP_subset_induct"
8.42 -
8.43 -val conjunctionD1 = thm "conjunctionD1"
8.44 -val conjunctionD2 = thm "conjunctionD2"
8.45 -
8.46 -
8.47 -fun mk_psimp thy globals R f_iff graph_is_function clause valthm =
8.48 - let
8.49 - val Globals {domT, z, ...} = globals
8.50 -
8.51 - val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause
8.52 - val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
8.53 - val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
8.54 - in
8.55 - ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
8.56 - |> (fn it => it COMP graph_is_function)
8.57 - |> implies_intr z_smaller
8.58 - |> forall_intr (cterm_of thy z)
8.59 - |> (fn it => it COMP valthm)
8.60 - |> implies_intr lhs_acc
8.61 - |> asm_simplify (HOL_basic_ss addsimps [f_iff])
8.62 - |> fold_rev (implies_intr o cprop_of) ags
8.63 - |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
8.64 - end
8.65 -
8.66 -
8.67 -
8.68 -fun mk_partial_induct_rule thy globals R complete_thm clauses =
8.69 - let
8.70 - val Globals {domT, x, z, a, P, D, ...} = globals
8.71 - val acc_R = mk_acc domT R
8.72 -
8.73 - val x_D = assume (cterm_of thy (Trueprop (D $ x)))
8.74 - val a_D = cterm_of thy (Trueprop (D $ a))
8.75 -
8.76 - val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x)))
8.77 -
8.78 - val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
8.79 - mk_forall x
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 (R $ Bound 0 $ x)
8.89 - $ Trueprop (P $ Bound 0))
8.90 - |> cterm_of thy
8.91 -
8.92 - val aihyp = assume ihyp
8.93 -
8.94 - fun prove_case clause =
8.95 - let
8.96 - val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, gs, lhs, rhs, case_hyp, ...}, RCs,
8.97 - qglr = (oqs, _, _, _), ...} = clause
8.98 -
8.99 - val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
8.100 - val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
8.101 - val sih = full_simplify replace_x_ss aihyp
8.102 -
8.103 - fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
8.104 - sih |> forall_elim (cterm_of thy rcarg)
8.105 - |> implies_elim_swp llRI
8.106 - |> fold_rev (implies_intr o cprop_of) CCas
8.107 - |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
8.108 -
8.109 - val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *)
8.110 -
8.111 - val step = Trueprop (P $ lhs)
8.112 - |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
8.113 - |> fold_rev (curry Logic.mk_implies) gs
8.114 - |> curry Logic.mk_implies (Trueprop (D $ lhs))
8.115 - |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
8.116 - |> cterm_of thy
8.117 -
8.118 - val P_lhs = assume step
8.119 - |> fold forall_elim cqs
8.120 - |> implies_elim_swp lhs_D
8.121 - |> fold_rev implies_elim_swp ags
8.122 - |> fold implies_elim_swp P_recs
8.123 -
8.124 - val res = cterm_of thy (Trueprop (P $ x))
8.125 - |> Simplifier.rewrite replace_x_ss
8.126 - |> symmetric (* P lhs == P x *)
8.127 - |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
8.128 - |> implies_intr (cprop_of case_hyp)
8.129 - |> fold_rev (implies_intr o cprop_of) ags
8.130 - |> fold_rev forall_intr cqs
8.131 - in
8.132 - (res, step)
8.133 - end
8.134 -
8.135 - val (cases, steps) = split_list (map prove_case clauses)
8.136 -
8.137 - val istep = complete_thm
8.138 - |> forall_elim_vars 0
8.139 - |> fold (curry op COMP) cases (* P x *)
8.140 - |> implies_intr ihyp
8.141 - |> implies_intr (cprop_of x_D)
8.142 - |> forall_intr (cterm_of thy x)
8.143 -
8.144 - val subset_induct_rule =
8.145 - acc_subset_induct
8.146 - |> (curry op COMP) (assume D_subset)
8.147 - |> (curry op COMP) (assume D_dcl)
8.148 - |> (curry op COMP) (assume a_D)
8.149 - |> (curry op COMP) istep
8.150 - |> fold_rev implies_intr steps
8.151 - |> implies_intr a_D
8.152 - |> implies_intr D_dcl
8.153 - |> implies_intr D_subset
8.154 -
8.155 - val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
8.156 -
8.157 - val simple_induct_rule =
8.158 - subset_induct_rule
8.159 - |> forall_intr (cterm_of thy D)
8.160 - |> forall_elim (cterm_of thy acc_R)
8.161 - |> assume_tac 1 |> Seq.hd
8.162 - |> (curry op COMP) (acc_downward
8.163 - |> (instantiate' [SOME (ctyp_of thy domT)]
8.164 - (map (SOME o cterm_of thy) [R, x, z]))
8.165 - |> forall_intr (cterm_of thy z)
8.166 - |> forall_intr (cterm_of thy x))
8.167 - |> forall_intr (cterm_of thy a)
8.168 - |> forall_intr (cterm_of thy P)
8.169 - in
8.170 - (subset_induct_all, simple_induct_rule)
8.171 - end
8.172 -
8.173 -
8.174 -
8.175 -(* Does this work with Guards??? *)
8.176 -fun mk_domain_intro thy globals R R_cases clause =
8.177 - let
8.178 - val Globals {z, domT, ...} = globals
8.179 - val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
8.180 - qglr = (oqs, _, _, _), ...} = clause
8.181 - val goal = Trueprop (mk_acc domT R $ lhs)
8.182 - |> fold_rev (curry Logic.mk_implies) gs
8.183 - |> cterm_of thy
8.184 - in
8.185 - Goal.init goal
8.186 - |> (SINGLE (resolve_tac [accI] 1)) |> the
8.187 - |> (SINGLE (eresolve_tac [forall_elim_vars 0 R_cases] 1)) |> the
8.188 - |> (SINGLE (CLASIMPSET auto_tac)) |> the
8.189 - |> Goal.conclude
8.190 - |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
8.191 - end
8.192 -
8.193 -
8.194 -fun maybe_mk_domain_intro thy =
8.195 - if !FundefCommon.domintros then mk_domain_intro thy
8.196 - else K (K (K (K refl)))
8.197 -
8.198 -
8.199 -fun mk_nest_term_case thy globals R' ihyp clause =
8.200 - let
8.201 - val Globals {x, z, ...} = globals
8.202 - val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
8.203 - qglr=(oqs, _, _, _), ...} = clause
8.204 -
8.205 - val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
8.206 -
8.207 - fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
8.208 - let
8.209 - val used = map (fn ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub)
8.210 -
8.211 - val hyp = Trueprop (R' $ arg $ lhs)
8.212 - |> fold_rev (curry Logic.mk_implies o prop_of) used
8.213 - |> FundefCtxTree.export_term (fixes, map prop_of assumes)
8.214 - |> fold_rev (curry Logic.mk_implies o prop_of) ags
8.215 - |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
8.216 - |> cterm_of thy
8.217 -
8.218 - val thm = assume hyp
8.219 - |> fold forall_elim cqs
8.220 - |> fold implies_elim_swp ags
8.221 - |> FundefCtxTree.import_thm thy (fixes, assumes) (* "(arg, lhs) : R'" *)
8.222 - |> fold implies_elim_swp used
8.223 -
8.224 - val acc = thm COMP ih_case
8.225 -
8.226 - val z_eq_arg = cterm_of thy (Trueprop (HOLogic.mk_eq (z, arg)))
8.227 -
8.228 - val arg_eq_z = (assume z_eq_arg) RS sym
8.229 -
8.230 - val z_acc = simplify (HOL_basic_ss addsimps [arg_eq_z]) acc (* fragile, slow... *)
8.231 - |> implies_intr (cprop_of case_hyp)
8.232 - |> implies_intr z_eq_arg
8.233 -
8.234 - val z_eq_arg = assume (cterm_of thy (Trueprop (mk_eq (z, arg))))
8.235 - val x_eq_lhs = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
8.236 -
8.237 - val ethm = (z_acc OF [z_eq_arg, x_eq_lhs])
8.238 - |> FundefCtxTree.export_thm thy (fixes,
8.239 - prop_of z_eq_arg :: prop_of x_eq_lhs :: map prop_of (ags @ assumes))
8.240 - |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
8.241 -
8.242 - val sub' = sub @ [(([],[]), acc)]
8.243 - in
8.244 - (sub', (hyp :: hyps, ethm :: thms))
8.245 - end
8.246 - | step _ _ _ _ = raise Match
8.247 - in
8.248 - FundefCtxTree.traverse_tree step tree
8.249 - end
8.250 -
8.251 -
8.252 -fun mk_nest_term_rule thy globals R R_cases clauses =
8.253 - let
8.254 - val Globals { domT, x, z, ... } = globals
8.255 - val acc_R = mk_acc domT R
8.256 -
8.257 - val R' = Free ("R", fastype_of R)
8.258 -
8.259 - val Rrel = Free ("R", mk_relT (domT, domT))
8.260 - val inrel_R = Const ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) $ Rrel
8.261 -
8.262 - val wfR' = cterm_of thy (Trueprop (Const ("FunDef.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
8.263 -
8.264 - (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
8.265 - val ihyp = all domT $ Abs ("z", domT,
8.266 - implies $ Trueprop (R' $ Bound 0 $ x)
8.267 - $ Trueprop (acc_R $ Bound 0))
8.268 - |> cterm_of thy
8.269 -
8.270 - val ihyp_a = assume ihyp |> forall_elim_vars 0
8.271 -
8.272 - val R_z_x = cterm_of thy (Trueprop (R $ z $ x))
8.273 -
8.274 - val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
8.275 - in
8.276 - R_cases
8.277 - |> forall_elim (cterm_of thy z)
8.278 - |> forall_elim (cterm_of thy x)
8.279 - |> forall_elim (cterm_of thy (acc_R $ z))
8.280 - |> curry op COMP (assume R_z_x)
8.281 - |> fold_rev (curry op COMP) cases
8.282 - |> implies_intr R_z_x
8.283 - |> forall_intr (cterm_of thy z)
8.284 - |> (fn it => it COMP accI)
8.285 - |> implies_intr ihyp
8.286 - |> forall_intr (cterm_of thy x)
8.287 - |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
8.288 - |> curry op RS (assume wfR')
8.289 - |> fold implies_intr hyps
8.290 - |> implies_intr wfR'
8.291 - |> forall_intr (cterm_of thy R')
8.292 - |> forall_elim (cterm_of thy (inrel_R))
8.293 - |> curry op RS wf_in_rel
8.294 - |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
8.295 - |> forall_intr (cterm_of thy Rrel)
8.296 - end
8.297 -
8.298 -
8.299 -
8.300 -
8.301 -fun mk_partial_rules thy data provedgoal =
8.302 - let
8.303 - val Prep {globals, G, f, R, clauses, values, R_cases, ex1_iff, ...} = data
8.304 -
8.305 - val provedgoal = PROFILE "Closing result" Goal.close_result provedgoal
8.306 -
8.307 - val graph_is_function = PROFILE "Getting function theorem" (fn x => (x COMP conjunctionD1) |> forall_elim_vars 0) provedgoal
8.308 -
8.309 - val complete_thm = PROFILE "Getting cases" (curry op COMP provedgoal) conjunctionD2
8.310 -
8.311 - val f_iff = PROFILE "Making f_iff" (curry op RS graph_is_function) ex1_iff
8.312 -
8.313 - val psimps = PROFILE "Proving simplification rules" (map2 (mk_psimp thy globals R f_iff graph_is_function)) clauses values
8.314 -
8.315 - val (subset_pinduct, simple_pinduct) = PROFILE "Proving partial induction rule"
8.316 - (mk_partial_induct_rule thy globals R complete_thm) clauses
8.317 -
8.318 - val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule thy globals R R_cases) clauses
8.319 -
8.320 - val dom_intros = PROFILE "Proving domain introduction rules" (map (maybe_mk_domain_intro thy globals R R_cases)) clauses
8.321 - in
8.322 - FundefResult {f=f, G=G, R=R, completeness=complete_thm,
8.323 - psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
8.324 - dom_intros=dom_intros}
8.325 - end
8.326 -
8.327 -
8.328 -end
8.329 -
8.330 -
9.1 --- a/src/HOL/Tools/function_package/inductive_wrap.ML Mon Jan 22 16:53:33 2007 +0100
9.2 +++ b/src/HOL/Tools/function_package/inductive_wrap.ML Mon Jan 22 17:29:43 2007 +0100
9.3 @@ -11,7 +11,7 @@
9.4 sig
9.5 val inductive_def : term list
9.6 -> ((bstring * typ) * mixfix) * local_theory
9.7 - -> thm list * (term * thm * local_theory)
9.8 + -> thm list * (term * thm * thm * local_theory)
9.9 end
9.10
9.11 structure FundefInductiveWrap =
9.12 @@ -40,7 +40,7 @@
9.13 let
9.14 val qdefs = map dest_all_all defs
9.15
9.16 - val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], ...}, lthy) =
9.17 + val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
9.18 InductivePackage.add_inductive_i true (*verbose*)
9.19 "" (* no altname *)
9.20 false (* no coind *)
9.21 @@ -70,7 +70,7 @@
9.22 |> Term.strip_comb |> snd |> hd (* Trueprop *)
9.23 |> Term.strip_comb |> fst
9.24 in
9.25 - (intrs, (Rdef_real, elim, lthy))
9.26 + (intrs, (Rdef_real, elim, induct, lthy))
9.27 end
9.28
9.29 end
10.1 --- a/src/HOL/Tools/function_package/mutual.ML Mon Jan 22 16:53:33 2007 +0100
10.2 +++ b/src/HOL/Tools/function_package/mutual.ML Mon Jan 22 17:29:43 2007 +0100
10.3 @@ -9,17 +9,16 @@
10.4 signature FUNDEF_MUTUAL =
10.5 sig
10.6
10.7 - val prepare_fundef_mutual : ((string * typ) * mixfix) list
10.8 + val prepare_fundef_mutual : FundefCommon.fundef_config
10.9 + -> string (* defname *)
10.10 + -> ((string * typ) * mixfix) list
10.11 -> term list
10.12 -> string (* default, unparsed term *)
10.13 -> local_theory
10.14 - -> ((FundefCommon.mutual_info * string * FundefCommon.prep_result) * local_theory)
10.15 -
10.16 -
10.17 - val mk_partial_rules_mutual : Proof.context -> FundefCommon.mutual_info -> FundefCommon.prep_result -> thm ->
10.18 - FundefCommon.fundef_mresult
10.19 -
10.20 - val sort_by_function : FundefCommon.mutual_info -> string list -> 'a list -> 'a list list
10.21 + -> ((thm (* goalstate *)
10.22 + * (thm -> FundefCommon.fundef_result) (* proof continuation *)
10.23 + * (thm list -> thm list list) (* sorting continuation *)
10.24 + ) * local_theory)
10.25
10.26 end
10.27
10.28 @@ -34,6 +33,45 @@
10.29 val sum_case_rules = thms "Datatype.sum.cases"
10.30 val split_apply = thm "Product_Type.split"
10.31
10.32 +type qgar = string * (string * typ) list * term list * term list * term
10.33 +
10.34 +fun name_of_fqgar (f, _, _, _, _) = f
10.35 +
10.36 +datatype mutual_part =
10.37 + MutualPart of
10.38 + {
10.39 + fvar : string * typ,
10.40 + cargTs: typ list,
10.41 + pthA: SumTools.sum_path,
10.42 + pthR: SumTools.sum_path,
10.43 + f_def: term,
10.44 +
10.45 + f: term option,
10.46 + f_defthm : thm option
10.47 + }
10.48 +
10.49 +
10.50 +datatype mutual_info =
10.51 + Mutual of
10.52 + {
10.53 + fsum_var : string * typ,
10.54 +
10.55 + ST: typ,
10.56 + RST: typ,
10.57 + streeA: SumTools.sum_tree,
10.58 + streeR: SumTools.sum_tree,
10.59 +
10.60 + parts: mutual_part list,
10.61 + fqgars: qgar list,
10.62 + qglrs: ((string * typ) list * term list * term * term) list,
10.63 +
10.64 + fsum : term option
10.65 + }
10.66 +
10.67 +
10.68 +
10.69 +
10.70 +
10.71
10.72
10.73 fun mutual_induct_Pnames n =
10.74 @@ -100,7 +138,7 @@
10.75 end;
10.76
10.77
10.78 -fun analyze_eqs ctxt fs eqs =
10.79 +fun analyze_eqs ctxt defname fs eqs =
10.80 let
10.81 val fnames = map fst fs
10.82 val (fqgars, arities) = fold_map (split_def ctxt fnames) eqs Symtab.empty
10.83 @@ -119,10 +157,9 @@
10.84 val (RST,streeR, pthsR) = SumTools.mk_tree_distinct resultTs
10.85 val (ST, streeA, pthsA) = SumTools.mk_tree argTs
10.86
10.87 - val def_name = foldr1 (fn (a,b) => a ^ "_" ^ b) (map Sign.base_name fnames)
10.88 val fsum_type = ST --> RST
10.89
10.90 - val ([fsum_var_name], _) = Variable.add_fixes [ def_name ^ "_sum" ] ctxt
10.91 + val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt
10.92 val fsum_var = (fsum_var_name, fsum_type)
10.93
10.94 fun define (fvar as (n, T)) caTs pthA pthR =
10.95 @@ -150,7 +187,7 @@
10.96
10.97 val qglrs = map convert_eqs fqgars
10.98 in
10.99 - Mutual {defname=def_name,fsum_var=fsum_var, ST=ST, RST=RST, streeA=streeA, streeR=streeR,
10.100 + Mutual {fsum_var=fsum_var, ST=ST, RST=RST, streeA=streeA, streeR=streeR,
10.101 parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE}
10.102 end
10.103
10.104 @@ -171,29 +208,15 @@
10.105 lthy')
10.106 end
10.107
10.108 - val Mutual { defname, fsum_var, ST, RST, streeA, streeR, parts, fqgars, qglrs, ... } = mutual
10.109 + val Mutual { fsum_var, ST, RST, streeA, streeR, parts, fqgars, qglrs, ... } = mutual
10.110 val (parts', lthy') = fold_map def (parts ~~ fixes) lthy
10.111 in
10.112 - (Mutual { defname=defname, fsum_var=fsum_var, ST=ST, RST=RST, streeA=streeA, streeR=streeR, parts=parts',
10.113 + (Mutual { fsum_var=fsum_var, ST=ST, RST=RST, streeA=streeA, streeR=streeR, parts=parts',
10.114 fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum },
10.115 lthy')
10.116 end
10.117
10.118
10.119 -fun prepare_fundef_mutual fixes eqss default lthy =
10.120 - let
10.121 - val mutual = analyze_eqs lthy (map fst fixes) eqss
10.122 - val Mutual {defname, fsum_var=(n, T), qglrs, ...} = mutual
10.123 -
10.124 - val (prep_result, fsum, lthy') =
10.125 - FundefPrep.prepare_fundef defname (n, T, NoSyn) qglrs default lthy
10.126 -
10.127 - val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
10.128 - in
10.129 - ((mutual', defname, prep_result), lthy'')
10.130 - end
10.131 -
10.132 -
10.133 (* Beta-reduce both sides of a meta-equality *)
10.134 fun beta_norm_eq thm =
10.135 let
10.136 @@ -315,7 +338,7 @@
10.137
10.138
10.139
10.140 -fun mk_partial_rules_mutual lthy (m as Mutual {RST, parts, streeR, fqgars, ...}) data prep_result =
10.141 +fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {RST, parts, streeR, fqgars, ...}) proof =
10.142 let
10.143 val thy = ProofContext.theory_of lthy
10.144
10.145 @@ -323,8 +346,9 @@
10.146 val expand = Assumption.export false lthy (LocalTheory.target_of lthy)
10.147 val expand_term = Drule.term_rule thy expand
10.148
10.149 - val result = FundefProof.mk_partial_rules thy data prep_result
10.150 - val FundefResult {f, G, R, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} = result
10.151 + val result = inner_cont proof
10.152 + val FundefResult {f, G, R, cases, psimps, trsimps, subset_pinducts=[subset_pinduct],simple_pinducts=[simple_pinduct],
10.153 + termination,domintros} = result
10.154
10.155 val all_f_defs = map (fn MutualPart {f_defthm = SOME f_def, cargTs, ...} =>
10.156 mk_applied_form lthy cargTs (symmetric (Thm.freezeT f_def)))
10.157 @@ -333,18 +357,19 @@
10.158 fun mk_mpsimp fqgar sum_psimp =
10.159 in_context lthy fqgar (recover_mutual_psimp thy RST streeR all_f_defs parts) sum_psimp
10.160
10.161 - val mpsimps = PROFILE "making mpsimps" (map2 mk_mpsimp fqgars) psimps
10.162 - val minducts = PROFILE "making mpinduct" (mutual_induct_rules thy simple_pinduct all_f_defs) m
10.163 - val termination = PROFILE "making mtermination" (full_simplify (HOL_basic_ss addsimps all_f_defs)) total_intro
10.164 + val mpsimps = map2 mk_mpsimp fqgars psimps
10.165 + val mtrsimps = map_option (map2 mk_mpsimp fqgars) trsimps
10.166 + val minducts = mutual_induct_rules thy simple_pinduct all_f_defs m
10.167 + val mtermination = full_simplify (HOL_basic_ss addsimps all_f_defs) termination
10.168 in
10.169 - FundefMResult { f=expand_term f, G=expand_term G, R=expand_term R,
10.170 - psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts,
10.171 - cases=expand completeness, termination=expand termination,
10.172 - domintros=map expand dom_intros }
10.173 + FundefResult { f=expand_term f, G=expand_term G, R=expand_term R,
10.174 + psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts,
10.175 + cases=expand cases, termination=expand mtermination,
10.176 + domintros=map_option (map expand) domintros,
10.177 + trsimps=map_option (map expand) trsimps}
10.178 end
10.179
10.180 -
10.181 -
10.182 +
10.183 (* puts an object in the "right bucket" *)
10.184 fun store_grouped P x [] = []
10.185 | store_grouped P x ((l, xs)::bs) =
10.186 @@ -356,5 +381,23 @@
10.187 (map (rpair []) names) (* in the empty buckets labeled with names *)
10.188
10.189 |> map (snd #> map snd) (* and remove the labels afterwards *)
10.190 +
10.191 +
10.192 +fun prepare_fundef_mutual config defname fixes eqss default lthy =
10.193 + let
10.194 + val mutual = analyze_eqs lthy defname (map fst fixes) eqss
10.195 + val Mutual {fsum_var=(n, T), qglrs, ...} = mutual
10.196 +
10.197 + val ((fsum, goalstate, cont), lthy') =
10.198 + FundefCore.prepare_fundef config defname (n, T, NoSyn) qglrs default lthy
10.199 +
10.200 + val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
10.201 +
10.202 + val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual'
10.203 + val sort_cont = sort_by_function mutual' (map (fst o fst) fixes)
10.204 + in
10.205 + ((goalstate, mutual_cont, sort_cont), lthy'')
10.206 + end
10.207 +
10.208
10.209 end
11.1 --- a/src/HOL/Tools/function_package/termination.ML Mon Jan 22 16:53:33 2007 +0100
11.2 +++ b/src/HOL/Tools/function_package/termination.ML Mon Jan 22 17:29:43 2007 +0100
11.3 @@ -9,7 +9,7 @@
11.4
11.5 signature FUNDEF_TERMINATION =
11.6 sig
11.7 - val mk_total_termination_goal : term -> term -> term
11.8 + val mk_total_termination_goal : term -> term
11.9 (* val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term*)
11.10 end
11.11
11.12 @@ -21,9 +21,9 @@
11.13 open FundefCommon
11.14 open FundefAbbrev
11.15
11.16 -fun mk_total_termination_goal f R =
11.17 +fun mk_total_termination_goal R =
11.18 let
11.19 - val domT = domain_type (fastype_of f)
11.20 + val domT = domain_type (fastype_of R)
11.21 val x = Free ("x", domT)
11.22 in
11.23 mk_forall x (Trueprop (mk_acc domT R $ x))
12.1 --- a/src/HOL/ex/Fundefs.thy Mon Jan 22 16:53:33 2007 +0100
12.2 +++ b/src/HOL/ex/Fundefs.thy Mon Jan 22 17:29:43 2007 +0100
12.3 @@ -24,7 +24,6 @@
12.4 text {* There is also a cases rule to distinguish cases along the definition *}
12.5 thm fib.cases
12.6
12.7 -thm fib.domintros
12.8
12.9 text {* total simp and induction rules: *}
12.10 thm fib.simps
12.11 @@ -172,8 +171,6 @@
12.12
12.13 thm evn_od.pinduct
12.14 thm evn_od.termination
12.15 -thm evn_od.domintros
12.16 -
12.17
12.18
12.19