# HG changeset patch # User krauss # Date 1150734334 -7200 # Node ID 984ae977f7aaceaed1f45ee4a930ca9ce57841b7 # Parent 2a48a5550045d03e1707b8796bef323e3f7ab274 Fixed name clash. Function-goals are now fully quantified. Avoiding large meta-conjunctions when setting up the goal. Cleanup. diff -r 2a48a5550045 -r 984ae977f7aa src/HOL/Tools/function_package/context_tree.ML --- a/src/HOL/Tools/function_package/context_tree.ML Mon Jun 19 18:02:49 2006 +0200 +++ b/src/HOL/Tools/function_package/context_tree.ML Mon Jun 19 18:25:34 2006 +0200 @@ -15,7 +15,7 @@ val cong_deps : thm -> int IntGraph.T val add_congs : thm list - val mk_tree: theory -> (thm * FundefCommon.depgraph) list -> term -> term -> FundefCommon.ctx_tree + val mk_tree: theory -> (thm * FundefCommon.depgraph) list -> term -> ProofContext.context -> term -> FundefCommon.ctx_tree val add_context_varnames : FundefCommon.ctx_tree -> string list -> string list @@ -70,45 +70,40 @@ (* Called on the INSTANTIATED branches of the congruence rule *) -fun mk_branch t = +fun mk_branch ctx t = let - val (fixes, impl) = dest_all_all t + val (ctx', fixes, impl) = dest_all_all_ctx ctx t val (assumes, term) = dest_implies_list impl in - (map dest_Free fixes, assumes, rhs_of term) + (ctx', fixes, assumes, rhs_of term) end - - - - - -fun find_cong_rule thy ((r,dep)::rs) t = +fun find_cong_rule thy ctx ((r,dep)::rs) t = (let val (c, subs) = (meta_rhs_of (concl_of r), prems_of r) val subst = Pattern.match thy (c, t) (Vartab.empty, Vartab.empty) - val branches = map (mk_branch o Envir.beta_norm o Envir.subst_vars subst) subs + val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_vars subst) subs in (r, dep, branches) end - handle Pattern.MATCH => find_cong_rule thy rs t) - | find_cong_rule thy [] _ = sys_error "function_package/context_tree.ML: No cong rule found!" + handle Pattern.MATCH => find_cong_rule thy ctx rs t) + | find_cong_rule thy _ [] _ = sys_error "function_package/context_tree.ML: No cong rule found!" fun matchcall f (a $ b) = if a = f then SOME b else NONE | matchcall f _ = NONE -fun mk_tree thy congs f t = +fun mk_tree thy congs f ctx t = case matchcall f t of - SOME arg => RCall (t, mk_tree thy congs f arg) + SOME arg => RCall (t, mk_tree thy congs f ctx arg) | NONE => if not (exists_Const (curry op = (dest_Const f)) t) then Leaf t else - let val (r, dep, branches) = find_cong_rule thy congs t in - Cong (t, r, dep, map (fn (fixes, assumes, st) => - (fixes, map (assume o cterm_of thy) assumes, mk_tree thy congs f st)) branches) + let val (r, dep, branches) = find_cong_rule thy ctx congs t in + Cong (t, r, dep, map (fn (ctx', fixes, assumes, st) => + (fixes, map (assume o cterm_of thy) assumes, mk_tree thy congs f ctx' st)) branches) end @@ -121,7 +116,7 @@ fun compose (fs1, as1) (fs2, as2) = (fs1 @ fs2, as1 @ as2) fun export_term (fixes, assumes) = - fold_rev (curry Logic.mk_implies) assumes #> fold (mk_forall o Free) fixes + fold_rev (curry Logic.mk_implies) assumes #> fold_rev (mk_forall o Free) fixes fun export_thm thy (fixes, assumes) = fold_rev (implies_intr o cterm_of thy) assumes @@ -194,18 +189,17 @@ fun rewrite_help fix f_as h_as x (Leaf t) = (reflexive (cterm_of thy t), x) | rewrite_help fix f_as h_as x (RCall (_ $ arg, st)) = let - val (inner, (Ri,ha)::x') = rewrite_help fix f_as h_as x st + val (inner, (lRi,ha)::x') = rewrite_help fix f_as h_as x st (* Need not use the simplifier here. Can use primitive steps! *) val rew_ha = if is_refl inner then I else simplify (HOL_basic_ss addsimps [inner]) val h_a_eq_h_a' = combination (reflexive (cterm_of thy h)) inner - val iRi = import_thm thy (fix, f_as) Ri (* a < lhs *) val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *) |> rew_ha val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih - val eq = implies_elim (implies_elim inst_ih iRi) iha + val eq = implies_elim (implies_elim inst_ih lRi) iha val h_a'_eq_f_a' = eq RS eq_reflection val result = transitive h_a_eq_h_a' h_a'_eq_f_a' diff -r 2a48a5550045 -r 984ae977f7aa src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Mon Jun 19 18:02:49 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_common.ML Mon Jun 19 18:25:34 2006 +0200 @@ -34,22 +34,20 @@ glrs: (term list * term list * term * term) list, glrs': (term list * term list * term * term) list, f_def: thm, - used: string list, - trees: ctx_tree list + ctx: ProofContext.context } datatype rec_call_info = RCInfo of { - RI: thm, - RIvs: (string * typ) list, - lRI: thm, - lRIq: thm, + RIvs: (string * typ) list, (* Call context: fixes and assumes *) + CCas: thm list, + rcarg: term, (* The recursive argument *) + + llRI: thm, Gh: thm, - Gh': thm, - GmAs: term list, - rcarg: term + Gh': thm } datatype clause_info = @@ -57,31 +55,28 @@ { no: int, + tree: ctx_tree, + case_hyp: thm, + qs: term list, gs: term list, lhs: term, rhs: term, cqs: cterm list, - cvqs: cterm list, ags: thm list, cqs': cterm list, ags': thm list, lhs': term, rhs': term, - ordcqs': cterm list, - GI: thm, lGI: thm, RCs: rec_call_info list, - tree: ctx_tree, - case_hyp: thm + ordcqs': cterm list } -type inj_proj = ((term -> term) * (term -> term)) - type qgar = (string * typ) list * term list * term list * term datatype mutual_part = @@ -115,9 +110,13 @@ Prep of { names: naming_context, - complete : term, - compat : term list, - clauses: clause_info list + goal: term, + goalI: thm, + values: thm list, + clauses: clause_info list, + + R_cases: thm, + ex1_iff: thm } datatype fundef_result = @@ -127,7 +126,6 @@ G : term, R : term, completeness : thm, - compatibility : thm list, psimps : thm list, subset_pinduct : thm, diff -r 2a48a5550045 -r 984ae977f7aa src/HOL/Tools/function_package/fundef_datatype.ML --- a/src/HOL/Tools/function_package/fundef_datatype.ML Mon Jun 19 18:02:49 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Mon Jun 19 18:25:34 2006 +0200 @@ -126,35 +126,34 @@ in o_alg thy P 2 [x] (map2 (pair o single) pats assums) |> fold_rev implies_intr hyps - |> zero_var_indexes - |> forall_intr_frees - |> forall_elim_vars 0 end fun pat_complete_tac i thm = let + val thy = theory_of_thm thm + val subgoal = nth (prems_of thm) (i - 1) - val assums = Logic.strip_imp_prems subgoal - val _ $ P = Logic.strip_imp_concl subgoal + + val ([P, x], subgf) = dest_all_all subgoal + + val assums = Logic.strip_imp_prems subgf fun pat_of assum = let val (qs, imp) = dest_all_all assum in case Logic.dest_implies imp of - (_ $ (_ $ x $ pat), _) => (x, (qs, pat)) + (_ $ (_ $ _ $ pat), _) => (qs, pat) | _ => raise COMPLETENESS end - val (x, (qss, pats)) = - case (map pat_of assums) of - [] => raise COMPLETENESS - | rs as ((x,_) :: _) - => (x, split_list (snd (split_list rs))) + val (qss, pats) = split_list (map pat_of assums) - val complete_thm = prove_completeness (theory_of_thm thm) x P qss pats + val complete_thm = prove_completeness thy x P qss pats + |> forall_intr (cterm_of thy x) + |> forall_intr (cterm_of thy P) in Seq.single (Drule.compose_single(complete_thm, i, thm)) end diff -r 2a48a5550045 -r 984ae977f7aa src/HOL/Tools/function_package/fundef_lib.ML --- a/src/HOL/Tools/function_package/fundef_lib.ML Mon Jun 19 18:02:49 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_lib.ML Mon Jun 19 18:25:34 2006 +0200 @@ -9,11 +9,12 @@ fun mk_forall (var as Free (v,T)) t = all T $ Abs (v,T, abstract_over (var,t)) - | mk_forall _ _ = raise Match + | mk_forall v _ = let val _ = print v in sys_error "mk_forall" end (* Builds a quantification with a new name for the variable. *) -fun mk_forall_rename ((v,T),newname) t = - all T $ Abs (newname,T, abstract_over (Free (v,T),t)) +fun mk_forall_rename (v as Free (_,T),newname) t = + all T $ Abs (newname, T, abstract_over (v, t)) + | mk_forall_rename (v, _) _ = let val _ = print v in sys_error "mk_forall_rename" end (* Constructs a tupled abstraction from an arbitrarily nested tuple of variables and a term. *) fun tupled_lambda vars t = @@ -44,6 +45,24 @@ end | dest_all_all t = ([],t) + +fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) = + let + val [(n', _)] = Variable.rename_wrt ctx [] [(n,T)] + val (_, ctx') = ProofContext.add_fixes_i [(n', SOME T, NoSyn)] ctx + + val (n'', body) = Term.dest_abs (n', T, b) + val _ = assert (n' = n'') "dest_all_ctx" (* Note: We assume that n' does not occur in the body. Otherwise it would be fixed. *) + + val (ctx'', vs, bd) = dest_all_all_ctx ctx' body + in + (ctx'', (n', T) :: vs, bd) + end + | dest_all_all_ctx ctx t = + (ctx, [], t) + + + (* unfold *) fun unfold P f g b x = if (P x) then ((f x)::(unfold P f g b (g x))) else (b x) @@ -56,11 +75,15 @@ | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs | map3 _ _ _ _ = raise Library.UnequalLengths; +fun map6 _ [] [] [] [] [] [] = [] + | map6 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) = f x y z u v w :: map6 f xs ys zs us vs ws + | map6 _ _ _ _ _ _ _ = raise Library.UnequalLengths; + (* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *) -fun upairs [] = [] - | upairs (x::xs) = map (pair x) (x::xs) @ upairs xs +fun unordered_pairs [] = [] + | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs fun the_single [x] = x diff -r 2a48a5550045 -r 984ae977f7aa src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Mon Jun 19 18:02:49 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_package.ML Mon Jun 19 18:25:34 2006 +0200 @@ -48,12 +48,11 @@ -fun fundef_afterqed congs curry_info name data names atts thmss thy = +fun fundef_afterqed congs mutual_info name data names atts [[result]] thy = let - val (complete_thm :: compat_thms) = map hd thmss - val fundef_data = FundefMutual.mk_partial_rules_mutual thy congs curry_info data (Thm.freezeT complete_thm) (map Thm.freezeT compat_thms) - val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, ...} = fundef_data - val Mutual {parts, ...} = curry_info + val fundef_data = FundefMutual.mk_partial_rules_mutual thy mutual_info data result + val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data + val Mutual {parts, ...} = mutual_info val Prep {names = Names {acc_R=accR, ...}, ...} = data val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR) @@ -62,13 +61,13 @@ val thy = fold2 (add_simps "psimps" []) (parts ~~ psimps) (names ~~ atts) thy val thy = thy |> Theory.add_path name - val (_, thy) = PureThy.add_thms [(("cases", complete_thm), [RuleCases.case_names (flat names)])] thy + val (_, thy) = PureThy.add_thms [(("cases", cases), [RuleCases.case_names (flat names)])] thy val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy - val (_, thy) = PureThy.add_thms [(("termination", termination), [])] thy + val (_, thy) = PureThy.add_thms [(("termination", standard termination), [])] thy val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names (flat names), InductAttrib.induct_set ""])] thy val thy = thy |> Theory.parent_path in - add_fundef_data name (fundef_data, curry_info, names, atts) thy + add_fundef_data name (fundef_data, mutual_info, names, atts) thy end fun gen_add_fundef prep_att eqns_attss thy = @@ -93,14 +92,14 @@ val t_eqns = map (map (Sign.read_prop thy)) eqns |> map (map (term_of o cterm_of thy)) (* HACK to prevent strange things from happening with abbreviations *) - val (curry_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqns thy - val Prep {complete, compat, ...} = data - - val props = (complete :: compat) (*(complete :: fst (chop 110 compat))*) + val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqns thy + val Prep {goal, goalI, ...} = data in thy |> ProofContext.init - |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs curry_info name data names atts) NONE ("", []) - (map (fn t => (("", []), [(t, [])])) props) + |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs mutual_info name data names atts) NONE ("", []) + [(("", []), [(goal, [])])] + |> Proof.refine (Method.primitive_text (fn _ => goalI)) + |> Seq.hd end @@ -167,7 +166,7 @@ in thy |> ProofContext.init |> ProofContext.note_thmss_i [(("termination", - [ContextRules.intro_query NONE]), [([termination], [])])] |> snd + [ContextRules.intro_query NONE]), [([standard termination], [])])] |> snd |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name mutual) NONE ("", []) [(("", []), [(goal, [])])] end diff -r 2a48a5550045 -r 984ae977f7aa src/HOL/Tools/function_package/fundef_prep.ML --- a/src/HOL/Tools/function_package/fundef_prep.ML Mon Jun 19 18:02:49 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_prep.ML Mon Jun 19 18:25:34 2006 +0200 @@ -18,13 +18,23 @@ -structure FundefPrep : FUNDEF_PREP = +structure FundefPrep (*: FUNDEF_PREP*) = struct open FundefCommon open FundefAbbrev +(* Theory dependencies. *) +val Pair_inject = thm "Product_Type.Pair_inject"; + +val acc_induct_rule = thm "Accessible_Part.acc_induct_rule" + +val ex1_implies_ex = thm "FunDef.fundef_ex1_existence" +val ex1_implies_un = thm "FunDef.fundef_ex1_uniqueness" +val ex1_implies_iff = thm "FunDef.fundef_ex1_iff" + +val conjunctionI = thm "conjunctionI"; @@ -37,15 +47,27 @@ end -fun build_tree thy f congs (qs, gs, lhs, rhs) = +fun build_tree thy f congs ctx (qs, gs, lhs, rhs) = let (* FIXME: Save precomputed dependencies in a theory data slot *) val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs) + + val (_(*FIXME*), ctx') = ProofContext.add_fixes_i (map (fn Free (n, T) => (n, SOME T, NoSyn)) qs) ctx in - FundefCtxTree.mk_tree thy congs_deps f rhs + FundefCtxTree.mk_tree thy congs_deps f ctx' rhs end +fun find_calls tree = + let + fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs) + | add_Ri _ _ _ _ = raise Match + in + rev (FundefCtxTree.traverse_tree add_Ri tree []) + end + + + (* maps (qs,gs,lhs,ths) to (qs',gs',lhs',rhs') with primed variables *) fun mk_primed_vars thy glrs = let @@ -63,104 +85,39 @@ end -fun mk_clause_info thy (names:naming_context) (no, (qs,gs,lhs,rhs)) (GI,tree) RIs = - let - val Names {domT, G, R, h, f, fvar, used, x, ...} = names - - val zv = Var (("z",0), domT) (* for generating h_assums *) - val xv = Var (("x",0), domT) - val rw_RI_to_h_assum = (mk_mem (mk_prod (zv, xv), R), - mk_mem (mk_prod (zv, h $ zv), G)) - val rw_f_to_h = (f, h) - - val cqs = map (cterm_of thy) qs - - val vqs = map free_to_var qs - val cvqs = map (cterm_of thy) vqs - - val ags = map (assume o cterm_of thy) gs - - val qs' = map (fn Free (v,T) => Free (variant used (v ^ "'"),T)) qs - val cqs' = map (cterm_of thy) qs' - - val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') [] - val ags' = map (assume o cterm_of thy o rename_vars) gs - val lhs' = rename_vars lhs - val rhs' = rename_vars rhs - - val localize = instantiate ([], cvqs ~~ cqs) - #> fold implies_elim_swp ags - - val GI = Thm.freezeT GI - val lGI = localize GI - - val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) [] o var_to_free) (term_vars (prop_of GI)) - - fun mk_call_info (RIvs, RI) = - let - fun mk_var0 (v,T) = Var ((v,0),T) - - val RI = Thm.freezeT RI - val lRI = localize RI - val lRIq = fold_rev (forall_intr o cterm_of thy o mk_var0) RIvs lRI - val plRI = prop_of lRI - val GmAs = Logic.strip_imp_prems plRI - val rcarg = case Logic.strip_imp_concl plRI of - trueprop $ (memb $ (pair $ rcarg $ _) $ R) => rcarg - | _ => raise Match - - val Gh_term = Pattern.rewrite_term thy [rw_RI_to_h_assum, rw_f_to_h] [] (prop_of lRIq) - val Gh = assume (cterm_of thy Gh_term) - val Gh' = assume (cterm_of thy (rename_vars Gh_term)) - in - RCInfo {RI=RI, RIvs=RIvs, lRI=lRI, lRIq=lRIq, Gh=Gh, Gh'=Gh', GmAs=GmAs, rcarg=rcarg} - end - - val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs)))) - in - ClauseInfo - { - no=no, - qs=qs, gs=gs, lhs=lhs, rhs=rhs, - cqs=cqs, cvqs=cvqs, ags=ags, - cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs', ordcqs' = ordcqs', - GI=GI, lGI=lGI, RCs=map mk_call_info RIs, - tree=tree, case_hyp = case_hyp - } - end - - - (* Chooses fresh free names, declares G and R, defines f and returns a record with all the information *) -fun setup_context (f, glrs, used) defname congs thy = +fun setup_context f glrs defname thy = let - val trees = map (build_tree thy f congs) glrs - val allused = fold FundefCtxTree.add_context_varnames trees used - val Const (f_fullname, fT) = f val fname = Sign.base_name f_fullname val domT = domain_type fT val ranT = range_type fT - val h = Free (variant allused "h", domT --> ranT) - val y = Free (variant allused "y", ranT) - val x = Free (variant allused "x", domT) - val z = Free (variant allused "z", domT) - val a = Free (variant allused "a", domT) - val D = Free (variant allused "D", HOLogic.mk_setT domT) - val P = Free (variant allused "P", domT --> boolT) - val Pbool = Free (variant allused "P", boolT) - val fvarname = variant allused "f" - val fvar = Free (fvarname, domT --> ranT) - val GT = mk_relT (domT, ranT) val RT = mk_relT (domT, domT) val G_name = defname ^ "_graph" val R_name = defname ^ "_rel" + val gfixes = [("h_fd", domT --> ranT), + ("y_fd", ranT), + ("x_fd", domT), + ("z_fd", domT), + ("a_fd", domT), + ("D_fd", HOLogic.mk_setT domT), + ("P_fd", domT --> boolT), + ("Pb_fd", boolT), + ("f_fd", fT)] + + val (fxnames, ctx) = (ProofContext.init thy) + |> ProofContext.add_fixes_i (map (fn (n,T) => (n, SOME T, NoSyn)) gfixes) + + val [h, y, x, z, a, D, P, Pbool, fvar] = map (fn (n,(_,T)) => Free (n, T)) (fxnames ~~ gfixes) + + val Free (fvarname, _) = fvar + val glrs' = mk_primed_vars thy glrs val thy = Sign.add_consts_i [(G_name, GT, NoSyn), (R_name, RT, NoSyn)] thy @@ -175,53 +132,24 @@ val ([f_def], thy) = PureThy.add_defs_i false [((fname ^ "_def", f_eq), [])] thy in - (Names {f=f, glrs=glrs, glrs'=glrs', fvar=fvar, fvarname=fvarname, domT=domT, ranT=ranT, G=G, R=R, acc_R=acc_R, h=h, x=x, y=y, z=z, a=a, D=D, P=P, Pbool=Pbool, f_def=f_def, used=allused, trees=trees}, thy) + (Names {f=f, glrs=glrs, glrs'=glrs', fvar=fvar, fvarname=fvarname, domT=domT, ranT=ranT, G=G, R=R, acc_R=acc_R, h=h, x=x, y=y, z=z, a=a, D=D, P=P, Pbool=Pbool, f_def=f_def, ctx=ctx}, thy) end -(* Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *) + + + +(* !!qs' qs. Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *) fun mk_compat_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) = (implies $ Trueprop (mk_eq (lhs, lhs')) $ Trueprop (mk_eq (rhs, rhs'))) |> fold_rev (curry Logic.mk_implies) (gs @ gs') - + |> fold_rev mk_forall (qs @ qs') (* all proof obligations *) fun mk_compat_proof_obligations glrs glrs' = - map (fn ((x,_), (_,y')) => mk_compat_impl (x,y')) (upairs (glrs ~~ glrs')) - - -fun extract_Ris thy congs f R tree (qs, gs, lhs, rhs) = - let - fun add_Ri2 (fixes,assumes) (_ $ arg) _ (_, x) = ([], (FundefCtxTree.export_term (fixes, map prop_of assumes) (mk_relmem (arg, lhs) R)) :: x) - | add_Ri2 _ _ _ _ = raise Match - - val preRis = rev (FundefCtxTree.traverse_tree add_Ri2 tree []) - val (vRis, preRis_unq) = split_list (map dest_all_all preRis) - - val Ris = map (fold_rev (curry Logic.mk_implies) gs) preRis_unq - in - (map (map dest_Free) vRis, preRis, Ris) - end + map (fn ((x,_), (_,y')) => mk_compat_impl (x,y')) (unordered_pairs (glrs ~~ glrs')) -fun mk_GIntro thy names (qs, gs, lhs, rhs) Ris = - let - val Names { domT, R, G, f, fvar, h, y, Pbool, ... } = names - - val z = Var (("z",0), domT) - val x = Var (("x",0), domT) - - val rew1 = (mk_mem (mk_prod (z, x), R), - mk_mem (mk_prod (z, fvar $ z), G)) - val rew2 = (f, fvar) - - val prems = map (Pattern.rewrite_term thy [rew1, rew2] []) Ris - val rhs' = Pattern.rewrite_term thy [rew2] [] rhs - in - mk_relmem (lhs, rhs') G - |> fold_rev (curry Logic.mk_implies) prems - |> fold_rev (curry Logic.mk_implies) gs - end fun mk_completeness names glrs = let @@ -234,61 +162,411 @@ in Trueprop Pbool |> fold_rev (curry Logic.mk_implies o mk_case) glrs + |> mk_forall_rename (x, "x") + |> mk_forall_rename (Pbool, "P") end -fun extract_conditions thy names trees congs = - let - val Names {f, R, glrs, glrs', ...} = names +fun inductive_def_wrap defs (thy, const) = + let + val qdefs = map dest_all_all defs - val (vRiss, preRiss, Riss) = split_list3 (map2 (extract_Ris thy congs f R) trees glrs) - val Gis = map2 (mk_GIntro thy names) glrs preRiss - val complete = mk_completeness names glrs - val compat = mk_compat_proof_obligations glrs glrs' - in - {G_intros = Gis, vRiss = vRiss, R_intross = Riss, complete = complete, compat = compat} - end - - -fun inductive_def defs (thy, const) = - let - val (thy, {intrs, elims = [elim], ...}) = - InductivePackage.add_inductive_i true (*verbose*) + val (thy, {intrs = intrs_gen, elims = [elim_gen], ...}) = + InductivePackage.add_inductive_i true (*verbose*) false (*add_consts*) "" (* no altname *) false (* no coind *) false (* elims, please *) false (* induction thm please *) [const] (* the constant *) - (map (fn t=>(("", t),[])) defs) (* the intros *) + (map (fn (_,t) => (("", t),[])) qdefs) (* the intros *) [] (* no special monos *) thy + +(* It would be nice if this worked... But this is actually HO-Unification... *) +(* fun inst (qs, intr) intr_gen = + Goal.init (cterm_of thy intr) + |> curry op COMP intr_gen + |> Goal.finish + |> fold_rev (forall_intr o cterm_of thy) qs*) + + fun inst (qs, intr) intr_gen = + intr_gen + |> Thm.freezeT + |> fold_rev (forall_intr o (fn Free (n, T) => cterm_of thy (Var ((n,0), T)))) qs + + val intrs = map2 inst qdefs intrs_gen + val elim = elim_gen + |> Thm.freezeT + |> forall_intr_vars (* FIXME *) in - (intrs, (thy, elim)) + (intrs, (thy, const, elim)) + end + + + + + +(* + * "!!qs xs. CS ==> G => (r, lhs) : R" + *) +fun mk_RIntro R (qs, gs, lhs, rhs) (rcfix, rcassm, rcarg) = + mk_relmem (rcarg, lhs) R + |> fold_rev (curry Logic.mk_implies o prop_of) rcassm + |> fold_rev (curry Logic.mk_implies) gs + |> fold_rev (mk_forall o Free) rcfix + |> fold_rev mk_forall qs + + +fun mk_GIntro thy f_const f_var G (qs, gs, lhs, rhs) RCs = + let + fun mk_h_assm (rcfix, rcassm, rcarg) = + mk_relmem (rcarg, f_var $ rcarg) G + |> fold_rev (curry Logic.mk_implies o prop_of) rcassm + |> fold_rev (mk_forall o Free) rcfix + in + mk_relmem (lhs, rhs) G + |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs + |> fold_rev (curry Logic.mk_implies) gs + |> Pattern.rewrite_term thy [(f_const, f_var)] [] + |> fold_rev mk_forall (f_var :: qs) + end + + + +fun mk_clause_info thy names no (qs,gs,lhs,rhs) tree RCs GIntro_thm RIntro_thms = + let + val Names {G, h, f, fvar, x, ...} = names + + val cqs = map (cterm_of thy) qs + val ags = map (assume o cterm_of thy) gs + + val used = [] (* XXX *) + (* FIXME: What is the relationship between this and mk_primed_vars? *) + val qs' = map (fn Free (v,T) => Free (variant used (v ^ "'"),T)) qs + val cqs' = map (cterm_of thy) qs' + + val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') [] + val ags' = map (assume o cterm_of thy o rename_vars) gs + val lhs' = rename_vars lhs + val rhs' = rename_vars rhs + + val lGI = GIntro_thm + |> forall_elim (cterm_of thy f) + |> fold forall_elim cqs + |> fold implies_elim_swp ags + + (* FIXME: Can be removed when inductive-package behaves nicely. *) + val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) []) + (term_frees (snd (dest_all_all (prop_of GIntro_thm)))) + + fun mk_call_info (rcfix, rcassm, rcarg) RI = + let + val crcfix = map (cterm_of thy o Free) rcfix + + val llRI = RI + |> fold forall_elim cqs + |> fold forall_elim crcfix + |> fold implies_elim_swp ags + |> fold implies_elim_swp rcassm + + val h_assum = + mk_relmem (rcarg, h $ rcarg) G + |> fold_rev (curry Logic.mk_implies o prop_of) rcassm + |> fold_rev (mk_forall o Free) rcfix + |> Pattern.rewrite_term thy [(f, h)] [] + + val Gh = assume (cterm_of thy h_assum) + val Gh' = assume (cterm_of thy (rename_vars h_assum)) + in + RCInfo {RIvs=rcfix, Gh=Gh, Gh'=Gh', rcarg=rcarg, CCas=rcassm, llRI=llRI} + end + + val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs)))) + + val RC_infos = map2 mk_call_info RCs RIntro_thms + in + ClauseInfo + { + no=no, + qs=qs, gs=gs, lhs=lhs, rhs=rhs, + cqs=cqs, ags=ags, + cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs', + lGI=lGI, RCs=RC_infos, + tree=tree, case_hyp = case_hyp, + ordcqs'=ordcqs' + } + end + + + + + +(* Copied from fundef_proof.ML: *) + +(***********************************************) +(* Compat thms are stored in normal form (with vars) *) + +(* replace this by a table later*) +fun store_compat_thms 0 thms = [] + | store_compat_thms n thms = + let + val (thms1, thms2) = chop n thms + in + (thms1 :: store_compat_thms (n - 1) thms2) + end + + +(* needs i <= j *) +fun lookup_compat_thm i j cts = + nth (nth cts (i - 1)) (j - i) +(***********************************************) + + +(* Returns "Gsi, Gsj', lhs_i = lhs_j' |-- rhs_j'_f = rhs_i_f" *) +(* if j < i, then turn around *) +fun get_compat_thm thy cts clausei clausej = + let + val ClauseInfo {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei + val ClauseInfo {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej + + val lhsi_eq_lhsj' = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj'))) + in if j < i then + let + val compat = lookup_compat_thm j i cts + in + compat (* "!!qj qi'. Gsj => Gsi' => lhsj = lhsi' ==> rhsj = rhsi'" *) + |> fold forall_elim (qsj' @ qsi) (* "Gsj' => Gsi => lhsj' = lhsi ==> rhsj' = rhsi" *) + |> fold implies_elim_swp gsj' + |> fold implies_elim_swp gsi + |> implies_elim_swp ((assume lhsi_eq_lhsj') RS sym) (* "Gsj', Gsi, lhsi = lhsj' |-- rhsj' = rhsi" *) + end + else + let + val compat = lookup_compat_thm i j cts + in + compat (* "!!qi qj'. Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *) + |> fold forall_elim (qsi @ qsj') (* "Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *) + |> fold implies_elim_swp gsi + |> fold implies_elim_swp gsj' + |> implies_elim_swp (assume lhsi_eq_lhsj') + |> (fn thm => thm RS sym) (* "Gsi, Gsj', lhsi = lhsj' |-- rhsj' = rhsi" *) + end end +(* Generates the replacement lemma with primed variables. A problem here is that one should not do +the complete requantification at the end to replace the variables. One should find a way to be more efficient +here. *) +fun mk_replacement_lemma thy (names:naming_context) ih_elim clause = + let + val Names {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names + val ClauseInfo {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause + + val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim + + val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs + val h_assums = map (fn RCInfo {Gh, ...} => Gh) RCs + val h_assums' = map (fn RCInfo {Gh', ...} => Gh') RCs + + val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *) + + val (eql, _) = FundefCtxTree.rewrite_by_tree thy f h ih_elim_case_inst (Ris ~~ h_assums) tree + + val replace_lemma = (eql RS meta_eq_to_obj_eq) + |> implies_intr (cprop_of case_hyp) + |> fold_rev (implies_intr o cprop_of) h_assums + |> fold_rev (implies_intr o cprop_of) ags + |> fold_rev forall_intr cqs + |> fold forall_elim cqs' + |> fold implies_elim_swp ags' + |> fold implies_elim_swp h_assums' + in + replace_lemma + end + + + + +fun mk_uniqueness_clause thy names compat_store clausei clausej RLj = + let + val Names {f, h, y, ...} = names + val ClauseInfo {no=i, lhs=lhsi, case_hyp, ...} = clausei + val ClauseInfo {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej + + val rhsj'h = Pattern.rewrite_term thy [(f,h)] [] rhsj' + val compat = get_compat_thm thy compat_store clausei clausej + val Ghsj' = map (fn RCInfo {Gh', ...} => Gh') RCsj + + val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h)))) + val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) + + val eq_pairs = assume (cterm_of thy (Trueprop (mk_eq (mk_prod (lhsi, y), mk_prod (lhsj',rhsj'h))))) + in + (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *) + |> implies_elim RLj (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *) + |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *) + |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *) + |> implies_intr (cprop_of y_eq_rhsj'h) + |> implies_intr (cprop_of lhsi_eq_lhsj') (* Gj', Rj1' ... Rjk' |-- [| lhs_i = lhs_j', y = rhs_j_h' |] ==> y = rhs_i_f *) + |> (fn it => Drule.compose_single(it, 2, Pair_inject)) (* Gj', Rj1' ... Rjk' |-- (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *) + |> implies_elim_swp eq_pairs + |> fold_rev (implies_intr o cprop_of) Ghsj' + |> fold_rev (implies_intr o cprop_of) gsj' (* Gj', Rj1', ..., Rjk' ==> (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *) + |> implies_intr (cprop_of eq_pairs) + |> fold_rev forall_intr ordcqs'j + end + + + +fun mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei = + let + val Names {x, y, G, fvar, f, ranT, ...} = names + val ClauseInfo {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei + + val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro + + fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case) + |> fold_rev (implies_intr o cprop_of) CCas + |> fold_rev (forall_intr o cterm_of thy o Free) RIvs + + val existence = lGI (*|> instantiate ([], [(cterm_of thy (free_to_var fvar), cterm_of thy f)])*) + |> fold (curry op COMP o prep_RC) RCs + + val a = cterm_of thy (mk_prod (lhs, y)) + val P = cterm_of thy (mk_eq (y, rhs)) + val a_in_G = assume (cterm_of thy (Trueprop (mk_mem (term_of a, G)))) + + val unique_clauses = map2 (mk_uniqueness_clause thy names compat_store clausei) clauses rep_lemmas + + val uniqueness = G_cases + |> forall_elim a + |> forall_elim P + |> implies_elim_swp a_in_G + |> fold implies_elim_swp unique_clauses + |> implies_intr (cprop_of a_in_G) + |> forall_intr (cterm_of thy y) + + val P2 = cterm_of thy (lambda y (mk_mem (mk_prod (lhs, y), G))) (* P2 y := (lhs, y): G *) + + val exactly_one = + ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhs)] + |> curry (op COMP) existence + |> curry (op COMP) uniqueness + |> simplify (HOL_basic_ss addsimps [case_hyp RS sym]) + |> implies_intr (cprop_of case_hyp) + |> fold_rev (implies_intr o cprop_of) ags + |> fold_rev forall_intr cqs + + val function_value = + existence + |> fold_rev (implies_intr o cprop_of) ags + |> implies_intr ihyp + |> implies_intr (cprop_of case_hyp) + |> forall_intr (cterm_of thy x) + |> forall_elim (cterm_of thy lhs) + |> curry (op RS) refl + in + (exactly_one, function_value) + end + + + + +fun prove_stuff thy congs names clauses complete compat compat_store G_elim R_elim = + let + val Names {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, Pbool, ...}:naming_context = names + + val f_def_fr = Thm.freezeT f_def + + val instantiate_and_def = (instantiate' [SOME (ctyp_of thy domT), SOME (ctyp_of thy ranT)] + [SOME (cterm_of thy f), SOME (cterm_of thy G)]) + #> curry op COMP (forall_intr_vars f_def_fr) + + val inst_ex1_ex = instantiate_and_def ex1_implies_ex + val inst_ex1_un = instantiate_and_def ex1_implies_un + val inst_ex1_iff = instantiate_and_def ex1_implies_iff + + (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) + val ihyp = all domT $ Abs ("z", domT, + implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R) + $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $ + Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G))) + |> cterm_of thy + + val ihyp_thm = assume ihyp |> forall_elim_vars 0 + val ih_intro = ihyp_thm RS inst_ex1_ex + val ih_elim = ihyp_thm RS inst_ex1_un + + val _ = Output.debug "Proving Replacement lemmas..." + val repLemmas = map (mk_replacement_lemma thy names ih_elim) clauses + + val _ = Output.debug "Proving cases for unique existence..." + val (ex1s, values) = split_list (map (mk_uniqueness_case thy names ihyp ih_intro G_elim compat_store clauses repLemmas) clauses) + + val _ = Output.debug "Proving: Graph is a function" (* FIXME: Rewrite this proof. *) + val graph_is_function = complete + |> forall_elim_vars 0 + |> fold (curry op COMP) ex1s + |> implies_intr (ihyp) + |> implies_intr (cterm_of thy (Trueprop (mk_mem (x, acc_R)))) + |> forall_intr (cterm_of thy x) + |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *) + |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it) + |> Drule.close_derivation + + val goal = complete COMP (graph_is_function COMP conjunctionI) + |> Drule.close_derivation + + val goalI = Goal.protect goal + |> fold_rev (implies_intr o cprop_of) compat + |> implies_intr (cprop_of complete) + in + (prop_of goal, goalI, inst_ex1_iff, values) + end + + + + + (* * This is the first step in a function definition. * * Defines the function, the graph and the termination relation, synthesizes completeness * and comatibility conditions and returns everything. *) -fun prepare_fundef thy congs defname f glrs used = +fun prepare_fundef thy congs defname f qglrs used = let - val (names, thy) = setup_context (f, glrs, used) defname congs thy - val Names {G, R, glrs, trees, ...} = names + val (names, thy) = setup_context f qglrs defname thy + val Names {G, R, ctx, glrs', fvar, ...} = names - val {G_intros, vRiss, R_intross, complete, compat} = extract_conditions thy names trees congs + + val n = length qglrs + val trees = map (build_tree thy f congs ctx) qglrs + val RCss = map find_calls trees + + val complete = mk_completeness names qglrs + |> cterm_of thy + |> assume - val (G_intro_thms, (thy, _)) = inductive_def G_intros (thy, G) - val (R_intro_thmss, (thy, _)) = fold_burrow inductive_def R_intross (thy, R) + val compat = mk_compat_proof_obligations qglrs glrs' + |> map (assume o cterm_of thy) + + val compat_store = compat + |> store_compat_thms n - val n = length glrs - val clauses = map3 (mk_clause_info thy names) ((1 upto n) ~~ glrs) (G_intro_thms ~~ trees) (map2 (curry op ~~) vRiss R_intro_thmss) + val R_intross = map2 (fn qglr => map (mk_RIntro R qglr)) qglrs RCss + val G_intros = map2 (mk_GIntro thy f fvar G) qglrs RCss + + val (GIntro_thms, (thy, _, G_elim)) = inductive_def_wrap G_intros (thy, G) + val (RIntro_thmss, (thy, _, R_elim)) = fold_burrow inductive_def_wrap R_intross (thy, R) + + val clauses = map6 (mk_clause_info thy names) (1 upto n) qglrs trees RCss GIntro_thms RIntro_thmss + + val (goal, goalI, ex1_iff, values) = prove_stuff thy congs names clauses complete compat compat_store G_elim R_elim in - (Prep {names = names, complete=complete, compat=compat, clauses = clauses}, + (Prep {names = names, goal = goal, goalI = goalI, values = values, clauses = clauses, ex1_iff = ex1_iff, R_cases = R_elim}, thy) end diff -r 2a48a5550045 -r 984ae977f7aa src/HOL/Tools/function_package/fundef_proof.ML --- a/src/HOL/Tools/function_package/fundef_proof.ML Mon Jun 19 18:02:49 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_proof.ML Mon Jun 19 18:25:34 2006 +0200 @@ -10,8 +10,8 @@ signature FUNDEF_PROOF = sig - val mk_partial_rules : theory -> thm list -> FundefCommon.prep_result - -> thm -> thm list -> FundefCommon.fundef_result + val mk_partial_rules : theory -> FundefCommon.prep_result + -> thm -> FundefCommon.fundef_result end @@ -37,8 +37,8 @@ val ex1_implies_iff = thm "fundef_ex1_iff" val acc_subset_induct = thm "acc_subset_induct" - - +val conjunctionD1 = thm "conjunctionD1" +val conjunctionD2 = thm "conjunctionD2" @@ -56,10 +56,6 @@ |> (fn it => it COMP valthm) |> implies_intr lhs_acc |> asm_simplify (HOL_basic_ss addsimps [f_iff]) -(* |> fold forall_intr cqs - |> forall_elim_vars 0 - |> varifyT - |> Drule.close_derivation*) end @@ -88,7 +84,7 @@ $ Trueprop (P $ Bound 0)) |> cterm_of thy - val aihyp = assume ihyp |> forall_elim_vars 0 + val aihyp = assume ihyp fun prove_case clause = let @@ -98,8 +94,13 @@ val lhs_D = simplify replace_x_ss x_D (* lhs : D *) val sih = full_simplify replace_x_ss aihyp - (* FIXME: Variable order destroyed by forall_intr_vars *) - val P_recs = map (fn RCInfo {lRI, RIvs, ...} => (lRI RS sih) |> forall_intr_vars) RCs (* [P rec1, P rec2, ... ] *) + fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = + sih |> forall_elim (cterm_of thy rcarg) + |> implies_elim_swp llRI + |> fold_rev (implies_intr o cprop_of) CCas + |> fold_rev (forall_intr o cterm_of thy o Free) RIvs + + val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *) val step = Trueprop (P $ lhs) |> fold_rev (curry Logic.mk_implies o prop_of) P_recs @@ -128,6 +129,7 @@ val (cases, steps) = split_list (map prove_case clauses) val istep = complete_thm + |> forall_elim_vars 0 |> fold (curry op COMP) cases (* P x *) |> implies_intr ihyp |> implies_intr (cprop_of x_D) @@ -164,8 +166,6 @@ - - (***********************************************) (* Compat thms are stored in normal form (with vars) *) @@ -187,7 +187,7 @@ (* recover the order of Vars *) fun get_var_order thy clauses = - map (fn (ClauseInfo {cqs,...}, ClauseInfo {cqs',...}) => map (cterm_of thy o free_to_var o term_of) (cqs @ cqs')) (upairs clauses) + map (fn (ClauseInfo {cqs,...}, ClauseInfo {cqs',...}) => map (cterm_of thy o free_to_var o term_of) (cqs @ cqs')) (unordered_pairs clauses) (* Returns "Gsi, Gsj', lhs_i = lhs_j' |-- rhs_j'_f = rhs_i_f" *) @@ -225,6 +225,8 @@ + + (* Generates the replacement lemma with primed variables. A problem here is that one should not do the complete requantification at the end to replace the variables. One should find a way to be more efficient here. *) @@ -235,7 +237,7 @@ val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim - val Ris = map (fn RCInfo {lRIq, ...} => lRIq) RCs + val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs val h_assums = map (fn RCInfo {Gh, ...} => Gh) RCs val h_assums' = map (fn RCInfo {Gh', ...} => Gh') RCs @@ -252,7 +254,7 @@ |> fold implies_elim_swp ags' |> fold implies_elim_swp h_assums' in - replace_lemma + replace_lemma end @@ -296,10 +298,9 @@ val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro - fun prep_RC (RCInfo {lRIq,RIvs, ...}) = lRIq - |> fold (forall_elim o cterm_of thy o Free) RIvs - |> (fn it => it RS ih_intro_case) - |> fold_rev (forall_intr o cterm_of thy o Free) RIvs + fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case) + |> fold_rev (implies_intr o cprop_of) CCas + |> fold_rev (forall_intr o cterm_of thy o Free) RIvs val existence = lGI |> instantiate ([], [(cterm_of thy (free_to_var fvar), cterm_of thy f)]) |> fold (curry op COMP o prep_RC) RCs @@ -353,7 +354,7 @@ in Goal.init goal |> (SINGLE (resolve_tac [accI] 1)) |> the - |> (SINGLE (eresolve_tac [R_cases] 1)) |> the + |> (SINGLE (eresolve_tac [forall_elim_vars 0 R_cases] 1)) |> the |> (SINGLE (CLASIMPSET auto_tac)) |> the |> Goal.conclude end @@ -453,74 +454,32 @@ |> fold implies_intr hyps |> implies_intr wfR' |> forall_intr (cterm_of thy R') - |> forall_elim_vars 0 - |> varifyT end -fun mk_partial_rules thy congs data complete_thm compat_thms = +fun mk_partial_rules thy data provedgoal = let - val Prep {names, clauses, complete, compat, ...} = data + val Prep {names, clauses, values, R_cases, ex1_iff, ...} = data val Names {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, ...}:naming_context = names -(* val _ = Output.debug "closing derivation: completeness" - val _ = Output.debug (Proofterm.size_of_proof (proof_of complete_thm)) - val _ = Output.debug (map (Proofterm.size_of_proof o proof_of) compat_thms)*) - val complete_thm = Drule.close_derivation complete_thm -(* val _ = Output.debug "closing derivation: compatibility"*) - val compat_thms = map Drule.close_derivation compat_thms -(* val _ = Output.debug " done"*) + val _ = print "Closing Derivation" - val complete_thm_fr = Thm.freezeT complete_thm - val compat_thms_fr = map Thm.freezeT compat_thms - val f_def_fr = Thm.freezeT f_def + val provedgoal = Drule.close_derivation provedgoal - val instantiate_and_def = (instantiate' [SOME (ctyp_of thy domT), SOME (ctyp_of thy ranT)] - [SOME (cterm_of thy f), SOME (cterm_of thy G)]) - #> curry op COMP (forall_intr_vars f_def_fr) - - val inst_ex1_ex = instantiate_and_def ex1_implies_ex - val inst_ex1_un = instantiate_and_def ex1_implies_un - val inst_ex1_iff = instantiate_and_def ex1_implies_iff + val _ = print "Getting gif" - (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) - val ihyp = all domT $ Abs ("z", domT, - implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R) - $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $ - Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G))) - |> cterm_of thy - - val ihyp_thm = assume ihyp - |> forall_elim_vars 0 - - val ih_intro = ihyp_thm RS inst_ex1_ex - val ih_elim = ihyp_thm RS inst_ex1_un + val graph_is_function = (provedgoal COMP conjunctionD1) + |> forall_elim_vars 0 - val _ = Output.debug "Proving Replacement lemmas..." - val repLemmas = map (mk_replacement_lemma thy names ih_elim) clauses + val _ = print "Getting cases" - val n = length clauses - val var_order = get_var_order thy clauses - val compat_store = store_compat_thms n (var_order ~~ compat_thms_fr) - - val R_cases = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const R)))))) |> Thm.freezeT - val G_cases = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const G)))))) |> Thm.freezeT - - val _ = Output.debug "Proving cases for unique existence..." - val (ex1s, values) = split_list (map (mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses repLemmas) clauses) + val complete_thm = provedgoal COMP conjunctionD2 - val _ = Output.debug "Proving: Graph is a function" - val graph_is_function = complete_thm_fr - |> fold (curry op COMP) ex1s - |> implies_intr (ihyp) - |> implies_intr (cterm_of thy (Trueprop (mk_mem (x, acc_R)))) - |> forall_intr (cterm_of thy x) - |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *) - |> Drule.close_derivation + val _ = print "making f_iff" - val f_iff = (graph_is_function RS inst_ex1_iff) + val f_iff = (graph_is_function RS ex1_iff) val _ = Output.debug "Proving simplification rules" val psimps = map2 (mk_psimp thy names f_iff graph_is_function) clauses values @@ -534,7 +493,7 @@ val _ = Output.debug "Proving domain introduction rules" val dom_intros = map (mk_domain_intro thy names R_cases) clauses in - FundefResult {f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm, + FundefResult {f=f, G=G, R=R, completeness=complete_thm, psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro, dom_intros=dom_intros} end diff -r 2a48a5550045 -r 984ae977f7aa src/HOL/Tools/function_package/mutual.ML --- a/src/HOL/Tools/function_package/mutual.ML Mon Jun 19 18:02:49 2006 +0200 +++ b/src/HOL/Tools/function_package/mutual.ML Mon Jun 19 18:25:34 2006 +0200 @@ -14,7 +14,7 @@ (FundefCommon.mutual_info * string * (FundefCommon.prep_result * theory)) - val mk_partial_rules_mutual : theory -> thm list -> FundefCommon.mutual_info -> FundefCommon.prep_result -> thm -> thm list -> + val mk_partial_rules_mutual : theory -> FundefCommon.mutual_info -> FundefCommon.prep_result -> thm -> FundefCommon.fundef_mresult end @@ -217,10 +217,10 @@ -fun mk_partial_rules_mutual thy congs (m as Mutual {qglrss, RST, parts, streeR, ...}) data complete_thm compat_thms = +fun mk_partial_rules_mutual thy (m as Mutual {qglrss, RST, parts, streeR, ...}) data result = let - val result = FundefProof.mk_partial_rules thy congs data complete_thm compat_thms - val FundefResult {f, G, R, compatibility, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} = result + val result = FundefProof.mk_partial_rules thy data result + val FundefResult {f, G, R, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} = result val sum_psimps = Library.unflat qglrss psimps diff -r 2a48a5550045 -r 984ae977f7aa src/HOL/ex/Fundefs.thy --- a/src/HOL/ex/Fundefs.thy Mon Jun 19 18:02:49 2006 +0200 +++ b/src/HOL/ex/Fundefs.thy Mon Jun 19 18:25:34 2006 +0200 @@ -135,8 +135,8 @@ "gcd3 0 y = y" "x < y \ gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)" "\ x < y \ gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)" - apply (cases xa, case_tac a, auto) - apply (case_tac b, auto) + apply (case_tac x, case_tac a, auto) + apply (case_tac ba, auto) done termination by (auto_term "measure (\(x,y). x + y)") @@ -152,6 +152,8 @@ "ev (2 * n) = True" "ev (2 * n + 1) = False" proof - -- {* completeness is more difficult here \dots *} + fix P :: bool + and x :: nat assume c1: "\n. x = 2 * n \ P" and c2: "\n. x = 2 * n + 1 \ P" have divmod: "x = 2 * (x div 2) + (x mod 2)" by auto