# HG changeset patch # User Christian Urban # Date 1293565885 0 # Node ID 8268b277d2402aafd22098073c33eee724aadd3d # Parent ffb5a181844b5cfc5b8749a1ebee515238a0c3c8 automated all strong induction lemmas diff -r ffb5a181844b -r 8268b277d240 Nominal/Ex/CoreHaskell.thy --- a/Nominal/Ex/CoreHaskell.thy Tue Dec 28 00:20:50 2010 +0000 +++ b/Nominal/Ex/CoreHaskell.thy Tue Dec 28 19:51:25 2010 +0000 @@ -93,6 +93,8 @@ thm core_haskell.distinct thm core_haskell.induct +thm core_haskell.inducts +thm core_haskell.strong_induct thm core_haskell.exhaust thm core_haskell.fv_defs thm core_haskell.bn_defs @@ -102,79 +104,6 @@ thm core_haskell.size_eqvt thm core_haskell.supp -lemma strong_induction_principle: - fixes c::"'a::fs" - assumes a01: "\b. P1 b KStar" - and a02: "\tkind1 tkind2 b. \\c. P1 c tkind1; \c. P1 c tkind2\ \ P1 b (KFun tkind1 tkind2)" - and a03: "\ty1 ty2 b. \\c. P3 c ty1; \c. P3 c ty2\ \ P2 b (CKEq ty1 ty2)" - and a04: "\tvar b. P3 b (TVar tvar)" - and a05: "\string b. P3 b (TC string)" - and a06: "\ty1 ty2 b. \\c. P3 c ty1; \c. P3 c ty2\ \ P3 b (TApp ty1 ty2)" - and a07: "\string ty_lst b. \\c. P4 c ty_lst\ \ P3 b (TFun string ty_lst)" - and a08: "\tvar tkind ty b. \\c. P1 c tkind; \c. P3 c ty; atom tvar \ b\ - \ P3 b (TAll tvar tkind ty)" - and a09: "\ck ty b. \\c. P2 c ck; \c. P3 c ty\ \ P3 b (TEq ck ty)" - and a10: "\b. P4 b TsNil" - and a11: "\ty ty_lst b. \\c. P3 c ty; \c. P4 c ty_lst\ \ P4 b (TsCons ty ty_lst)" - and a12: "\string b. P5 b (CVar string)" - and a12a:"\str b. P5 b (CConst str)" - and a13: "\co1 co2 b. \\c. P5 c co1; \c. P5 c co2\ \ P5 b (CApp co1 co2)" - and a14: "\string co_lst b. \\c. P6 c co_lst\ \ P5 b (CFun string co_lst)" - and a15: "\tvar ckind co b. \\c. P2 c ckind; \c. P5 c co; atom tvar \ b\ - \ P5 b (CAll tvar ckind co)" - and a16: "\ck co b. \\c. P2 c ck; \c. P5 c co\ \ P5 b (CEq ck co)" - and a17: "\ty b. \\c. P3 c ty\ \ P5 b (CRefl ty)" - and a17a: "\co b. \\c. P5 c co\ \ P5 b (CSym co)" - and a18: "\co1 co2 b. \\c. P5 c co1; \c. P5 c co2\ \ P5 b (CCir co1 co2)" - and a18a:"\co ty b. \\c. P5 c co; \c. P3 c ty\ \ P5 b (CAt co ty)" - and a19: "\co b. \\c. P5 c co\ \ P5 b (CLeft co)" - and a20: "\co b. \\c. P5 c co\ \ P5 b (CRight co)" - and a21: "\co1 co2 b. \\c. P5 c co1; \c. P5 c co2\ \ P5 b (CSim co1 co2)" - and a22: "\co b. \\c. P5 c co\ \ P5 b (CRightc co)" - and a23: "\co b. \\c. P5 c co\ \ P5 b (CLeftc co)" - and a24: "\co1 co2 b. \\c. P5 c co1; \c. P5 c co2\ \ P5 b (CCoe co1 co2)" - and a25: "\b. P6 b CsNil" - and a26: "\co co_lst b. \\c. P5 c co; \c. P6 c co_lst\ \ P6 b (CsCons co co_lst)" - and a27: "\var b. P7 b (Var var)" - and a28: "\string b. P7 b (K string)" - and a29: "\tvar tkind trm b. \\c. P1 c tkind; \c. P7 c trm; atom tvar \ b\ - \ P7 b (LAMT tvar tkind trm)" - and a30: "\tvar ckind trm b. \\c. P2 c ckind; \c. P7 c trm; atom tvar \ b\ - \ P7 b (LAMC tvar ckind trm)" - and a31: "\trm ty b. \\c. P7 c trm; \c. P3 c ty\ \ P7 b (AppT trm ty)" - and a31a:"\trm co b. \\c. P7 c trm; \c. P5 c co\ \ P7 b (AppC trm co)" - and a32: "\var ty trm b. \\c. P3 c ty; \c. P7 c trm; atom var \ b\ \ P7 b (Lam var ty trm)" - and a33: "\trm1 trm2 b. \\c. P7 c trm1; \c. P7 c trm2\ \ P7 b (App trm1 trm2)" - and a34: "\var ty trm1 trm2 b. \\c. P3 c ty; \c. P7 c trm1; \c. P7 c trm2; atom var \ b\ - \ P7 b (Let var ty trm1 trm2)" - and a35: "\trm assoc_lst b. \\c. P7 c trm; \c. P8 c assoc_lst\ \ P7 b (Case trm assoc_lst)" - and a36: "\trm ty b. \\c. P7 c trm; \c. P3 c ty\ \ P7 b (Cast trm ty)" - and a37: "\b. P8 b ANil" - and a38: "\pt trm assoc_lst b. \\c. P9 c pt; \c. P7 c trm; \c. P8 c assoc_lst; set (bv (pt)) \* b\ - \ P8 b (ACons pt trm assoc_lst)" - and a39: "\string tvars cvars vars b. \\c. P11 c tvars; \c. P12 c cvars; \c. P10 c vars\ - \ P9 b (Kpat string tvars cvars vars)" - and a40: "\b. P10 b VsNil" - and a41: "\var ty vars b. \\c. P3 c ty; \c. P10 c vars\ \ P10 b (VsCons var ty vars)" - and a42: "\b. P11 b TvsNil" - and a43: "\tvar tkind tvars b. \\c. P1 c tkind; \c. P11 c tvars\ - \ P11 b (TvsCons tvar tkind tvars)" - and a44: "\b. P12 b CvsNil" - and a45: "\tvar ckind cvars b. \\c. P2 c ckind; \c. P12 c cvars\ - \ P12 b (CvsCons tvar ckind cvars)" - shows "P1 c tkind" - "P2 c ckind" - "P3 c ty" - "P4 c ty_lst" - "P5 c co" - "P6 c co_lst" - "P7 c trm" - "P8 c assoc_lst" - "P9 c pt" - "P10 c vars" - "P11 c tvars" - "P12 c cvars" -oops end diff -r ffb5a181844b -r 8268b277d240 Nominal/Ex/Foo1.thy --- a/Nominal/Ex/Foo1.thy Tue Dec 28 00:20:50 2010 +0000 +++ b/Nominal/Ex/Foo1.thy Tue Dec 28 19:51:25 2010 +0000 @@ -44,6 +44,7 @@ thm foo.induct thm foo.inducts thm foo.exhaust +thm foo.strong_induct thm foo.strong_exhaust thm foo.fv_defs thm foo.bn_defs @@ -57,32 +58,6 @@ thm foo.fresh thm foo.bn_finite -lemma - fixes t::trm - and as::assg - and as'::assg' - and c::"'a::fs" - assumes a1: "\x c. P1 c (Var x)" - and a2: "\t1 t2 c. \\d. P1 d t1; \d. P1 d t2\ \ P1 c (App t1 t2)" - and a3: "\x t c. \{atom x} \* c; \d. P1 d t\ \ P1 c (Lam x t)" - and a4: "\as t c. \set (bn1 as) \* c; \d. P2 d as; \d. P1 d t\ \ P1 c (Let1 as t)" - and a5: "\as t c. \set (bn2 as) \* c; \d. P2 d as; \d. P1 d t\ \ P1 c (Let2 as t)" - and a6: "\as t c. \set (bn3 as) \* c; \d. P2 d as; \d. P1 d t\ \ P1 c (Let3 as t)" - and a7: "\as' t c. \(bn4 as') \* c; \d. P3 d as'; \d. P1 d t\ \ P1 c (Let4 as' t)" - and a8: "\x y t c. \d. P1 d t \ P2 c (As x y t)" - and a9: "\c. P3 c (BNil)" - and a10: "\c a as. \d. P3 d as \ P3 c (BAs a as)" - shows "P1 c t" "P2 c as" "P3 c as'" -apply(raw_tactic {* Induction_Schema.induction_schema_tac @{context} @{thms assms} *}) -apply(rule_tac y="t" and c="c" in foo.strong_exhaust(1)) -apply(simp_all)[7] -apply(rule_tac ya="as"in foo.strong_exhaust(2)) -apply(simp_all)[1] -apply(rule_tac yb="as'" in foo.strong_exhaust(3)) -apply(simp_all)[2] -apply(relation "measure (sum_case (size o snd) (sum_case (size o snd) (size o snd)))") -apply(simp_all add: foo.size) -done end diff -r ffb5a181844b -r 8268b277d240 Nominal/Ex/Foo2.thy --- a/Nominal/Ex/Foo2.thy Tue Dec 28 00:20:50 2010 +0000 +++ b/Nominal/Ex/Foo2.thy Tue Dec 28 19:51:25 2010 +0000 @@ -9,6 +9,7 @@ atom_decl name + nominal_datatype foo: trm = Var "name" | App "trm" "trm" @@ -25,7 +26,6 @@ | "bn (As_Nil) = []" - thm foo.bn_defs thm foo.permute_bn thm foo.perm_bn_alpha @@ -35,6 +35,7 @@ thm foo.distinct thm foo.induct thm foo.inducts +thm foo.strong_induct thm foo.exhaust thm foo.strong_exhaust thm foo.fv_defs @@ -47,432 +48,8 @@ thm foo.fsupp thm foo.supp thm foo.fresh - -ML {* - -open Function_Lib - -type rec_call_info = int * (string * typ) list * term list * term list - -datatype scheme_case = SchemeCase of - {bidx : int, - qs: (string * typ) list, - oqnames: string list, - gs: term list, - lhs: term list, - rs: rec_call_info list} - -datatype scheme_branch = SchemeBranch of - {P : term, - xs: (string * typ) list, - ws: (string * typ) list, - Cs: term list} - -datatype ind_scheme = IndScheme of - {T: typ, (* sum of products *) - branches: scheme_branch list, - cases: scheme_case list} - -val ind_atomize = Raw_Simplifier.rewrite true @{thms induct_atomize} -val ind_rulify = Raw_Simplifier.rewrite true @{thms induct_rulify} - -fun meta thm = thm RS eq_reflection - -val sum_prod_conv = Raw_Simplifier.rewrite true - (map meta (@{thm split_conv} :: @{thms sum.cases})) - -fun term_conv thy cv t = - cv (cterm_of thy t) - |> prop_of |> Logic.dest_equals |> snd - -fun mk_relT T = HOLogic.mk_setT (HOLogic.mk_prodT (T, T)) - -fun dest_hhf ctxt t = - let - val ((vars, imp), ctxt') = Function_Lib.focus_term t ctxt - in - (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp) - end - -fun mk_scheme' ctxt cases concl = - let - fun mk_branch concl = - let - val _ = tracing ("concl:\n" ^ Syntax.string_of_term ctxt concl) - val (_, ws, Cs, _ $ Pxs) = dest_hhf ctxt concl - val (P, xs) = strip_comb Pxs - val _ = tracing ("xs: " ^ commas (map @{make_string} xs)) - val _ = map dest_Free xs - val _ = tracing ("done") - in - SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs } - end - - val (branches, cases') = (* correction *) - case Logic.dest_conjunctions concl of - [conc] => - let - val _ $ Pxs = Logic.strip_assums_concl conc - val (P, _) = strip_comb Pxs - val (cases', conds) = - take_prefix (Term.exists_subterm (curry op aconv P)) cases - val concl' = fold_rev (curry Logic.mk_implies) conds conc - in - ([mk_branch concl'], cases') - end - | concls => (map mk_branch concls, cases) - - fun mk_case premise = - let - val (ctxt', qs, prems, _ $ Plhs) = dest_hhf ctxt premise - val (P, lhs) = strip_comb Plhs - - fun bidx Q = - find_index (fn SchemeBranch {P=P',...} => Q aconv P') branches - - fun mk_rcinfo pr = - let - val (_, Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr - val (P', rcs) = strip_comb Phyp - in - (bidx P', Gvs, Gas, rcs) - end - - fun is_pred v = exists (fn SchemeBranch {P,...} => v aconv P) branches - - val (gs, rcprs) = - take_prefix (not o Term.exists_subterm is_pred) prems - in - SchemeCase {bidx=bidx P, qs=qs, oqnames=map fst qs(*FIXME*), - gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs} - end - - fun PT_of (SchemeBranch { xs, ...}) = - foldr1 HOLogic.mk_prodT (map snd xs) - - val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches) - in - IndScheme {T=ST, cases=map mk_case cases', branches=branches } - end - -fun mk_completeness ctxt (IndScheme {cases, branches, ...}) bidx = - let - val SchemeBranch { xs, ws, Cs, ... } = nth branches bidx - val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases - - val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases [] - val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs)) - val Cs' = map (Pattern.rewrite_term (ProofContext.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs - - fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) = - HOLogic.mk_Trueprop Pbool - |> fold_rev (fn x_l => curry Logic.mk_implies (HOLogic.mk_Trueprop(HOLogic.mk_eq x_l))) - (xs' ~~ lhs) - |> fold_rev (curry Logic.mk_implies) gs - |> fold_rev mk_forall_rename (oqnames ~~ map Free qs) - in - HOLogic.mk_Trueprop Pbool - |> fold_rev (curry Logic.mk_implies o mk_case) relevant_cases - |> fold_rev (curry Logic.mk_implies) Cs' - |> fold_rev (Logic.all o Free) ws - |> fold_rev mk_forall_rename (map fst xs ~~ xs') - |> mk_forall_rename ("P", Pbool) - end - -fun mk_wf R (IndScheme {T, ...}) = - HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R) - -fun mk_ineqs R (IndScheme {T, cases, branches}) = - let - fun inject i ts = - SumTree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts) - - val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *) - - fun mk_pres bdx args = - let - val SchemeBranch { xs, ws, Cs, ... } = nth branches bdx - fun replace (x, v) t = betapply (lambda (Free x) t, v) - val Cs' = map (fold replace (xs ~~ args)) Cs - val cse = - HOLogic.mk_Trueprop thesis - |> fold_rev (curry Logic.mk_implies) Cs' - |> fold_rev (Logic.all o Free) ws - in - Logic.mk_implies (cse, HOLogic.mk_Trueprop thesis) - end - - fun f (SchemeCase {bidx, qs, oqnames, gs, lhs, rs, ...}) = - let - fun g (bidx', Gvs, Gas, rcarg) = - let val export = - fold_rev (curry Logic.mk_implies) Gas - #> fold_rev (curry Logic.mk_implies) gs - #> fold_rev (Logic.all o Free) Gvs - #> fold_rev mk_forall_rename (oqnames ~~ map Free qs) - in - (HOLogic.mk_mem (HOLogic.mk_prod (inject bidx' rcarg, inject bidx lhs), R) - |> HOLogic.mk_Trueprop - |> export, - mk_pres bidx' rcarg - |> export - |> Logic.all thesis) - end - in - map g rs - end - in - map f cases - end - - -fun mk_ind_goal thy branches = - let - fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) = - HOLogic.mk_Trueprop (list_comb (P, map Free xs)) - |> fold_rev (curry Logic.mk_implies) Cs - |> fold_rev (Logic.all o Free) ws - |> term_conv thy ind_atomize - |> Object_Logic.drop_judgment thy - |> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs)) - in - SumTree.mk_sumcases HOLogic.boolT (map brnch branches) - end - -fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss - (IndScheme {T, cases=scases, branches}) = - let - val n = length branches - val scases_idx = map_index I scases - - fun inject i ts = - SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts) - val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches) - - val thy = ProofContext.theory_of ctxt - val cert = cterm_of thy - - val P_comp = mk_ind_goal thy branches +thm foo.size - (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) - val ihyp = Term.all T $ Abs ("z", T, - Logic.mk_implies - (HOLogic.mk_Trueprop ( - Const (@{const_name Set.member}, HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) - $ (HOLogic.pair_const T T $ Bound 0 $ x) - $ R), - HOLogic.mk_Trueprop (P_comp $ Bound 0))) - |> cert - - val aihyp = Thm.assume ihyp - - (* Rule for case splitting along the sum types *) - val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches - val pats = map_index (uncurry inject) xss - val sum_split_rule = - Pat_Completeness.prove_completeness thy [x] (P_comp $ x) xss (map single pats) - - fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) = - let - val fxs = map Free xs - val branch_hyp = Thm.assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat)))) - - val C_hyps = map (cert #> Thm.assume) Cs - - val (relevant_cases, ineqss') = - (scases_idx ~~ ineqss) - |> filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx) - |> split_list - - fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press = - let - val case_hyps = - map (Thm.assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs) - - val cqs = map (cert o Free) qs - val ags = map (Thm.assume o cert) gs - - val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps) - val sih = full_simplify replace_x_ss aihyp - - fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) = - let - val cGas = map (Thm.assume o cert) Gas - val cGvs = map (cert o Free) Gvs - val import = fold Thm.forall_elim (cqs @ cGvs) - #> fold Thm.elim_implies (ags @ cGas) - val ipres = pres - |> Thm.forall_elim (cert (list_comb (P_of idx, rcargs))) - |> import - in - sih - |> Thm.forall_elim (cert (inject idx rcargs)) - |> Thm.elim_implies (import ineq) (* Psum rcargs *) - |> Conv.fconv_rule sum_prod_conv - |> Conv.fconv_rule ind_rulify - |> (fn th => th COMP ipres) (* P rs *) - |> fold_rev (Thm.implies_intr o cprop_of) cGas - |> fold_rev Thm.forall_intr cGvs - end - - val P_recs = map2 mk_Prec rs ineq_press (* [P rec1, P rec2, ... ] *) - - val step = HOLogic.mk_Trueprop (list_comb (P, lhs)) - |> fold_rev (curry Logic.mk_implies o prop_of) P_recs - |> fold_rev (curry Logic.mk_implies) gs - |> fold_rev (Logic.all o Free) qs - |> cert - - val Plhs_to_Pxs_conv = - foldl1 (uncurry Conv.combination_conv) - (Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps) - - val res = Thm.assume step - |> fold Thm.forall_elim cqs - |> fold Thm.elim_implies ags - |> fold Thm.elim_implies P_recs (* P lhs *) - |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *) - |> fold_rev (Thm.implies_intr o cprop_of) (ags @ case_hyps) - |> fold_rev Thm.forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *) - in - (res, (cidx, step)) - end - - val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss') - - val bstep = complete_thm - |> Thm.forall_elim (cert (list_comb (P, fxs))) - |> fold (Thm.forall_elim o cert) (fxs @ map Free ws) - |> fold Thm.elim_implies C_hyps - |> fold Thm.elim_implies cases (* P xs *) - |> fold_rev (Thm.implies_intr o cprop_of) C_hyps - |> fold_rev (Thm.forall_intr o cert o Free) ws - - val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x)) - |> Goal.init - |> (Simplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases})) - THEN CONVERSION ind_rulify 1) - |> Seq.hd - |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep) - |> Goal.finish ctxt - |> Thm.implies_intr (cprop_of branch_hyp) - |> fold_rev (Thm.forall_intr o cert) fxs - in - (Pxs, steps) - end - - val (branches, steps) = - map_index prove_branch (branches ~~ (complete_thms ~~ pats)) - |> split_list |> apsnd flat - - val istep = sum_split_rule - |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches - |> Thm.implies_intr ihyp - |> Thm.forall_intr (cert x) (* "!!x. (!!y P x" *) - - val induct_rule = - @{thm "wf_induct_rule"} - |> (curry op COMP) wf_thm - |> (curry op COMP) istep - - val steps_sorted = map snd (sort (int_ord o pairself fst) steps) - in - (steps_sorted, induct_rule) - end - - -fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts = - (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL (SUBGOAL (fn (t, i) => - let - val (ctxt', _, cases, concl) = dest_hhf ctxt t - val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl - val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt' - val R = Free (Rn, mk_relT ST) - val x = Free (xn, ST) - val cert = cterm_of (ProofContext.theory_of ctxt) - - val ineqss = mk_ineqs R scheme - |> map (map (pairself (Thm.assume o cert))) - val complete = - map_range (mk_completeness ctxt scheme #> cert #> Thm.assume) (length branches) - val wf_thm = mk_wf R scheme |> cert |> Thm.assume - - val (descent, pres) = split_list (flat ineqss) - val newgoals = complete @ pres @ wf_thm :: descent - - val (steps, indthm) = - mk_induct_rule ctxt'' R x complete wf_thm ineqss scheme - - fun project (i, SchemeBranch {xs, ...}) = - let - val inst = (foldr1 HOLogic.mk_prod (map Free xs)) - |> SumTree.mk_inj ST (length branches) (i + 1) - |> cert - in - indthm - |> Drule.instantiate' [] [SOME inst] - |> simplify SumTree.sumcase_split_ss - |> Conv.fconv_rule ind_rulify - end - - val res = Conjunction.intr_balanced (map_index project branches) - |> fold_rev Thm.implies_intr (map cprop_of newgoals @ steps) - |> Drule.generalize ([], [Rn]) - - val nbranches = length branches - val npres = length pres - in - Thm.compose_no_flatten false (res, length newgoals) i - THEN term_tac (i + nbranches + npres) - THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches)))) - THEN (EVERY (map (TRY o comp_tac) ((i + nbranches - 1) downto i))) - end)) - - -fun induction_schema_tac ctxt = - mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt; - -*} - -ML {* -val trm1 = @{prop "P1 &&& P2 &&& P3"} -val trm2 = @{prop "(P1 &&& P2) &&& P3 &&& P4"} -*} - -ML {* - Logic.dest_conjunctions trm2 -*} - -lemma - shows "P1" "P2" "P4" -oops - -lemma - shows "P1" "P2" "P3" "P4" -oops - -lemma strong_induct: - fixes c :: "'a :: fs" - and assg :: assg and trm :: trm - assumes a0: "\name c. P1 c (Var name)" - and a1: "\trm1 trm2 c. \\d. P1 d trm1; \d. P1 d trm2\ \ P1 c (App trm1 trm2)" - and a2: "\name trm c. (\d. P1 d trm) \ P1 c (Lam name trm)" - and a3: "\a1 t1 a2 t2 c. - \((set (bn a1)) \ (set (bn a2))) \* c; \d. P2 c a1; \d. P1 d t1; \d. P2 d a2; \d. P1 d t2\ - \ P1 c (Let1 a1 t1 a2 t2)" - and a4: "\n1 n2 t1 t2 c. - \({atom n1} \ {atom n2}) \* c; \d. P1 d t1; \d. P1 d t2\ \ P1 c (Let2 n1 n2 t1 t2)" - and a5: "\c. P2 c As_Nil" - and a6: "\name1 name2 trm assg c. \\d. P1 d trm; \d. P2 d assg\ \ P2 c (As name1 name2 trm assg)" - shows "P1 c trm" "P2 c assg" - apply(raw_tactic {* induction_schema_tac @{context} @{thms assms} *}) - apply(rule_tac y="trm" and c="c" in foo.strong_exhaust(1)) - apply(simp_all)[5] - apply(rule_tac ya="assg" in foo.strong_exhaust(2)) - apply(simp_all)[2] - apply(relation "measure (sum_case (size o snd) (size o snd))") - apply(simp_all add: foo.size) - done end diff -r ffb5a181844b -r 8268b277d240 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Tue Dec 28 00:20:50 2010 +0000 +++ b/Nominal/Ex/Lambda.thy Tue Dec 28 19:51:25 2010 +0000 @@ -20,33 +20,12 @@ thm lam.size_eqvt -section {* Strong Induction Lemma via Induct_schema *} - - -lemma strong_induct: - fixes c::"'a::fs" - assumes a1: "\name c. P c (Var name)" - and a2: "\lam1 lam2 c. \\d. P d lam1; \d. P d lam2\ \ P c (App lam1 lam2)" - and a3: "\name lam c. \{atom name} \* c; \d. P d lam\ \ P c (Lam name lam)" - shows "P c lam" -using assms -apply(induction_schema) -apply(rule_tac y="lam" in lam.strong_exhaust) -apply(blast) -apply(blast) -apply(blast) -apply(relation "measure (\(x,y). size y)") -apply(simp_all add: lam.size) -done - section {* Typing *} nominal_datatype ty = TVar string -| TFun ty ty +| TFun ty ty ("_ \ _") -notation - TFun ("_ \ _") (* declare ty.perm[eqvt] diff -r ffb5a181844b -r 8268b277d240 Nominal/Ex/Let.thy --- a/Nominal/Ex/Let.thy Tue Dec 28 00:20:50 2010 +0000 +++ b/Nominal/Ex/Let.thy Tue Dec 28 19:51:25 2010 +0000 @@ -30,278 +30,7 @@ thm trm_assn.exhaust thm trm_assn.strong_exhaust -lemma - fixes t::trm - and as::assn - and c::"'a::fs" - assumes a1: "\x c. P1 c (Var x)" - and a2: "\t1 t2 c. \\d. P1 d t1; \d. P1 d t2\ \ P1 c (App t1 t2)" - and a3: "\x t c. \{atom x} \* c; \d. P1 d t\ \ P1 c (Lam x t)" - and a4: "\as t c. \set (bn as) \* c; \d. P2 d as; \d. P1 d t\ \ P1 c (Let as t)" - and a5: "\c. P2 c ANil" - and a6: "\x t as c. \\d. P1 d t; \d. P2 d as\ \ P2 c (ACons x t as)" - shows "P1 c t" "P2 c as" -using assms -apply(induction_schema) -apply(rule_tac y="t" in trm_assn.strong_exhaust(1)) -apply(blast) -apply(blast) -apply(blast) -apply(blast) -apply(rule_tac ya="as" in trm_assn.strong_exhaust(2)) -apply(blast) -apply(blast) -apply(relation "measure (sum_case (\y. size (snd y)) (\z. size (snd z)))") -apply(simp_all add: trm_assn.size) -done - -text {* *} - - (* -proof - - have x: "\(p::perm) (c::'a::fs). P1 c (p \ t)" - and y: "\(p::perm) (c::'a::fs). P2 c (p \ as)" - apply(induct rule: trm_assn.inducts) - apply(simp) - apply(rule a1) - apply(simp) - apply(rule a2) - apply(assumption) - apply(assumption) - -- "lam case" - apply(simp) - apply(subgoal_tac "\q. (q \ {atom (p \ name)}) \* c \ supp (Lam (p \ name) (p \ trm)) \* q") - apply(erule exE) - apply(erule conjE) - apply(drule supp_perm_eq[symmetric]) - apply(simp) - apply(thin_tac "?X = ?Y") - apply(rule a3) - apply(simp add: atom_eqvt permute_set_eq) - apply(simp only: permute_plus[symmetric]) - apply(rule at_set_avoiding2) - apply(simp add: finite_supp) - apply(simp add: finite_supp) - apply(simp add: finite_supp) - apply(simp add: freshs fresh_star_def) - --"let case" - apply(simp) - thm trm_assn.eq_iff - thm eq_iffs - apply(subgoal_tac "\q. (q \ set (bn (p \ assn))) \* c \ supp (Abs_lst (bn (p \ assn)) (p \ trm)) \* q") - apply(erule exE) - apply(erule conjE) - prefer 2 - apply(rule at_set_avoiding2) - apply(rule fin_bn) - apply(simp add: finite_supp) - apply(simp add: finite_supp) - apply(simp add: abs_fresh) - apply(rule_tac t = "Let (p \ assn) (p \ trm)" in subst) - prefer 2 - apply(rule a4) - prefer 4 - apply(simp add: eq_iffs) - apply(rule conjI) - prefer 2 - apply(simp add: set_eqvt trm_assn.fv_bn_eqvt) - apply(subst permute_plus[symmetric]) - apply(blast) - prefer 2 - apply(simp add: eq_iffs) - thm eq_iffs - apply(subst permute_plus[symmetric]) - apply(blast) - apply(simp add: supps) - apply(simp add: fresh_star_def freshs) - apply(drule supp_perm_eq[symmetric]) - apply(simp) - apply(simp add: eq_iffs) - apply(simp) - apply(thin_tac "?X = ?Y") - apply(rule a4) - apply(simp add: set_eqvt trm_assn.fv_bn_eqvt) - apply(subst permute_plus[symmetric]) - apply(blast) - apply(subst permute_plus[symmetric]) - apply(blast) - apply(simp add: supps) - thm at_set_avoiding2 - --"HERE" - apply(rule at_set_avoiding2) - apply(rule fin_bn) - apply(simp add: finite_supp) - apply(simp add: finite_supp) - apply(simp add: fresh_star_def freshs) - apply(rule ballI) - apply(simp add: eqvts permute_bn) - apply(rule a5) - apply(simp add: permute_bn) - apply(rule a6) - apply simp - apply simp - done - then have a: "P1 c (0 \ t)" by blast - have "P2 c (permute_bn 0 (0 \ l))" using b' by blast - then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all -qed -*) - -text {* *} - -(* - -primrec - permute_bn_raw -where - "permute_bn_raw pi (Lnil_raw) = Lnil_raw" -| "permute_bn_raw pi (Lcons_raw a t l) = Lcons_raw (pi \ a) t (permute_bn_raw pi l)" - -quotient_definition - "permute_bn :: perm \ lts \ lts" -is - "permute_bn_raw" - -lemma [quot_respect]: "((op =) ===> alpha_lts_raw ===> alpha_lts_raw) permute_bn_raw permute_bn_raw" - apply simp - apply clarify - apply (erule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.inducts) - apply (rule TrueI)+ - apply simp_all - apply (rule_tac [!] alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros) - apply simp_all - done - -lemmas permute_bn = permute_bn_raw.simps[quot_lifted] - -lemma permute_bn_zero: - "permute_bn 0 a = a" - apply(induct a rule: trm_lts.inducts(2)) - apply(rule TrueI)+ - apply(simp_all add:permute_bn) - done - -lemma permute_bn_add: - "permute_bn (p + q) a = permute_bn p (permute_bn q a)" - oops - -lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)" - apply(induct lts rule: trm_lts.inducts(2)) - apply(rule TrueI)+ - apply(simp_all add:permute_bn eqvts trm_lts.eq_iff) - done - -lemma perm_bn: - "p \ bn l = bn(permute_bn p l)" - apply(induct l rule: trm_lts.inducts(2)) - apply(rule TrueI)+ - apply(simp_all add:permute_bn eqvts) - done - -lemma fv_perm_bn: - "fv_bn l = fv_bn (permute_bn p l)" - apply(induct l rule: trm_lts.inducts(2)) - apply(rule TrueI)+ - apply(simp_all add:permute_bn eqvts) - done - -lemma Lt_subst: - "supp (Abs_lst (bn lts) trm) \* q \ (Lt lts trm) = Lt (permute_bn q lts) (q \ trm)" - apply (simp add: trm_lts.eq_iff permute_bn_alpha_bn) - apply (rule_tac x="q" in exI) - apply (simp add: alphas) - apply (simp add: perm_bn[symmetric]) - apply(rule conjI) - apply(drule supp_perm_eq) - apply(simp add: abs_eq_iff) - apply(simp add: alphas_abs alphas) - apply(drule conjunct1) - apply (simp add: trm_lts.supp) - apply(simp add: supp_abs) - apply (simp add: trm_lts.supp) - done - - -lemma fin_bn: - "finite (set (bn l))" - apply(induct l rule: trm_lts.inducts(2)) - apply(simp_all add:permute_bn eqvts) - done - -thm trm_lts.inducts[no_vars] - -lemma - fixes t::trm - and l::lts - and c::"'a::fs" - assumes a1: "\name c. P1 c (Vr name)" - and a2: "\trm1 trm2 c. \\d. P1 d trm1; \d. P1 d trm2\ \ P1 c (Ap trm1 trm2)" - and a3: "\name trm c. \atom name \ c; \d. P1 d trm\ \ P1 c (Lm name trm)" - and a4: "\lts trm c. \set (bn lts) \* c; \d. P2 d lts; \d. P1 d trm\ \ P1 c (Lt lts trm)" - and a5: "\c. P2 c Lnil" - and a6: "\name trm lts c. \\d. P1 d trm; \d. P2 d lts\ \ P2 c (Lcons name trm lts)" - shows "P1 c t" and "P2 c l" -proof - - have "(\(p::perm) (c::'a::fs). P1 c (p \ t))" and - b': "(\(p::perm) (q::perm) (c::'a::fs). P2 c (permute_bn p (q \ l)))" - apply(induct rule: trm_lts.inducts) - apply(simp) - apply(rule a1) - apply(simp) - apply(rule a2) - apply(simp) - apply(simp) - apply(simp) - apply(subgoal_tac "\q. (q \ (atom (p \ name))) \ c \ supp (Lm (p \ name) (p \ trm)) \* q") - apply(erule exE) - apply(rule_tac t="Lm (p \ name) (p \ trm)" - and s="q\ Lm (p \ name) (p \ trm)" in subst) - apply(rule supp_perm_eq) - apply(simp) - apply(simp) - apply(rule a3) - apply(simp add: atom_eqvt) - apply(subst permute_plus[symmetric]) - apply(blast) - apply(rule at_set_avoiding2_atom) - apply(simp add: finite_supp) - apply(simp add: finite_supp) - apply(simp add: fresh_def) - apply(simp add: trm_lts.fv[simplified trm_lts.supp]) - apply(simp) - apply(subgoal_tac "\q. (q \ set (bn (p \ lts))) \* c \ supp (Abs_lst (bn (p \ lts)) (p \ trm)) \* q") - apply(erule exE) - apply(erule conjE) - thm Lt_subst - apply(subst Lt_subst) - apply assumption - apply(rule a4) - apply(simp add:perm_bn[symmetric]) - apply(simp add: eqvts) - apply (simp add: fresh_star_def fresh_def) - apply(rotate_tac 1) - apply(drule_tac x="q + p" in meta_spec) - apply(simp) - apply(rule at_set_avoiding2) - apply(rule fin_bn) - apply(simp add: finite_supp) - apply(simp add: finite_supp) - apply(simp add: fresh_star_def fresh_def supp_abs) - apply(simp add: eqvts permute_bn) - apply(rule a5) - apply(simp add: permute_bn) - apply(rule a6) - apply simp - apply simp - done - then have a: "P1 c (0 \ t)" by blast - have "P2 c (permute_bn 0 (0 \ l))" using b' by blast - then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all -qed - - - lemma lets_bla: "x \ z \ y \ z \ x \ y \(Lt (Lcons x (Vr y) Lnil) (Vr x)) \ (Lt (Lcons x (Vr z) Lnil) (Vr x))" by (simp add: trm_lts.eq_iff) diff -r ffb5a181844b -r 8268b277d240 Nominal/Ex/Multi_Recs2.thy --- a/Nominal/Ex/Multi_Recs2.thy Tue Dec 28 00:20:50 2010 +0000 +++ b/Nominal/Ex/Multi_Recs2.thy Tue Dec 28 19:51:25 2010 +0000 @@ -104,23 +104,21 @@ and "\pat1 pat2 c. \\c. P6 c pat1; \c. P6 c pat2\ \ P6 c (PPair pat1 pat2)" shows "P1 c exp" and "P2 c fnclause" and "P3 c fnclauses" and "P4 c lrb" and "P5 c lrbs" and "P6 c pat" apply(raw_tactic {* Induction_Schema.induction_schema_tac @{context} @{thms assms} *}) -oops - -ML {* - val trm1 = @{prop "P1 &&& P2 &&& P3"} - val trm2 = @{prop "(P1 &&& P2) &&& P3 &&& P4"} -*} - -ML {* - Logic.dest_conjunction_list trm1; - Logic.dest_conjunction_list trm2 -*} - -ML {* - Logic.dest_conjunctions trm1; - Logic.dest_conjunctions trm2 -*} - + apply(rule_tac y="exp" and c="c" in fun_recs.strong_exhaust(1)) + apply(simp_all)[4] + apply(rule_tac ya="fnclause" and c="c" in fun_recs.strong_exhaust(2)) + apply(simp_all)[1] + apply(rule_tac yb="fnclauses" in fun_recs.strong_exhaust(3)) + apply(simp_all)[2] + apply(rule_tac yc="lrb" in fun_recs.strong_exhaust(4)) + apply(simp_all)[1] + apply(rule_tac yd="lrbs" in fun_recs.strong_exhaust(5)) + apply(simp_all)[2] + apply(rule_tac ye="pat" in fun_recs.strong_exhaust(6)) + apply(simp_all)[3] + apply(tactic {* prove_termination_ind @{context} 1 *}) + apply(simp_all add: fun_recs.size) + done end diff -r ffb5a181844b -r 8268b277d240 Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Tue Dec 28 00:20:50 2010 +0000 +++ b/Nominal/Ex/TypeSchemes.thy Tue Dec 28 19:51:25 2010 +0000 @@ -38,7 +38,7 @@ All2 xs::"name fset" ty::"ty2" bind (res) xs in ty thm tys2.distinct -thm tys2.induct +thm tys2.induct tys2.strong_induct thm tys2.exhaust tys2.strong_exhaust thm tys2.fv_defs thm tys2.bn_defs @@ -50,18 +50,6 @@ thm tys2.supp thm tys2.fresh -lemma strong_induct: - fixes c::"'a::fs" - assumes "\names ty2 c. fset (map_fset atom names) \* c \ P c (All2 names ty2)" - shows "P c tys" -using assms -apply(induction_schema) -apply(rule_tac y="tys" in tys2.strong_exhaust) -apply(blast) -apply(relation "measure (\(x,y). size y)") -apply(simp_all add: tys2.size) -done - text {* Some Tests *} diff -r ffb5a181844b -r 8268b277d240 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Tue Dec 28 00:20:50 2010 +0000 +++ b/Nominal/Nominal2.thy Tue Dec 28 19:51:25 2010 +0000 @@ -535,7 +535,7 @@ val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs' qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms - val qstrong_induct_thm = prove_strong_induct lthyC qinduct qstrong_exhaust_thms bclauses + val qstrong_induct_thms = prove_strong_induct lthyC qinduct qstrong_exhaust_thms qsize_simps bclauses (* noting the theorems *) @@ -558,6 +558,7 @@ ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts) ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) ||>> Local_Theory.note ((thms_suffix "strong_exhaust", []), qstrong_exhaust_thms) + ||>> Local_Theory.note ((thms_suffix "strong_induct", []), qstrong_induct_thms) ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) diff -r ffb5a181844b -r 8268b277d240 Nominal/nominal_dt_quot.ML --- a/Nominal/nominal_dt_quot.ML Tue Dec 28 00:20:50 2010 +0000 +++ b/Nominal/nominal_dt_quot.ML Tue Dec 28 19:51:25 2010 +0000 @@ -42,7 +42,8 @@ val prove_strong_exhausts: Proof.context -> thm list -> bclause list list list -> thm list -> thm list -> thm list -> thm list -> thm list -> thm list - val prove_strong_induct: Proof.context -> thm -> thm list -> bclause list list list -> thm + val prove_strong_induct: Proof.context -> thm -> thm list -> thm list -> bclause list list list -> + thm list end structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = @@ -668,7 +669,7 @@ mk_full_horn (params @ [(c_name, c_ty)]) prems'' concl' end -fun prove_strong_induct lthy induct exhausts bclausesss = +fun prove_strong_induct lthy induct exhausts size_thms bclausesss = let val ((insts, [induct']), lthy') = Variable.import true [induct] lthy @@ -706,17 +707,16 @@ end) ctxt THEN_ALL_NEW asm_full_simp_tac HOL_basic_ss - val thm = Goal.prove_multi lthy'' [] prems' concls + val size_simp_tac = + simp_tac (size_simpset addsimps (@{thms comp_def snd_conv} @ size_thms)) + in + Goal.prove_multi lthy'' [] prems' concls (fn {prems, context} => - print_tac "start" - THEN Induction_Schema.induction_schema_tac context prems - THEN print_tac "after induct schema" + Induction_Schema.induction_schema_tac context prems THEN RANGE (map (pat_tac context) exhausts) 1 - THEN print_tac "after pat" - THEN Skip_Proof.cheat_tac (ProofContext.theory_of context) - ) - in - @{thm TrueI} + THEN prove_termination_ind context 1 + THEN ALLGOALS size_simp_tac) + |> ProofContext.export lthy'' lthy end diff -r ffb5a181844b -r 8268b277d240 Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Tue Dec 28 00:20:50 2010 +0000 +++ b/Nominal/nominal_dt_rawfuns.ML Tue Dec 28 19:51:25 2010 +0000 @@ -142,7 +142,7 @@ val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs Function_Common.default_config (pat_completeness_simp constr_thms) lthy - val (info, lthy2) = prove_termination size_thms (Local_Theory.restore lthy1) + val (info, lthy2) = prove_termination_fun size_thms (Local_Theory.restore lthy1) val {fs, simps, inducts, ...} = info val raw_bn_induct = (the inducts) @@ -277,7 +277,7 @@ val (_, lthy') = Function.add_function all_fun_names all_fun_eqs Function_Common.default_config (pat_completeness_simp constr_thms) lthy - val (info, lthy'') = prove_termination size_simps (Local_Theory.restore lthy') + val (info, lthy'') = prove_termination_fun size_simps (Local_Theory.restore lthy') val {fs, simps, inducts, ...} = info; @@ -342,7 +342,7 @@ val (_, lthy') = Function.add_function all_fun_names all_fun_eqs Function_Common.default_config (pat_completeness_simp (prod_simps @ cns_thms)) lthy - val (info, lthy'') = prove_termination size_thms (Local_Theory.restore lthy') + val (info, lthy'') = prove_termination_fun size_thms (Local_Theory.restore lthy') val {fs, simps, ...} = info; diff -r ffb5a181844b -r 8268b277d240 Nominal/nominal_library.ML --- a/Nominal/nominal_library.ML Tue Dec 28 00:20:50 2010 +0000 +++ b/Nominal/nominal_library.ML Tue Dec 28 19:51:25 2010 +0000 @@ -116,8 +116,10 @@ val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list (* tactics for function package *) + val size_simpset: simpset val pat_completeness_simp: thm list -> Proof.context -> tactic - val prove_termination: thm list -> Proof.context -> Function.info * local_theory + val prove_termination_ind: Proof.context -> int -> tactic + val prove_termination_fun: thm list -> Proof.context -> Function.info * local_theory (* transformations of premises in inductions *) val transform_prem1: Proof.context -> string list -> thm -> thm @@ -473,45 +475,69 @@ THEN ALLGOALS (asm_full_simp_tac simp_set) end +(* simpset for size goals *) +val size_simpset = HOL_ss + addsimprocs Nat_Numeral_Simprocs.cancel_numerals + addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral + zero_less_Suc prod.size(1) mult_Suc_right} -fun prove_termination_tac size_simps ctxt = +val natT = @{typ nat} + +fun prod_size_const T1 T2 = let - val natT = @{typ nat} - fun prod_size_const fT sT = - let - val fT_fun = fT --> natT - val sT_fun = sT --> natT - val prodT = Type (@{type_name prod}, [fT, sT]) - in - Const (@{const_name prod_size}, [fT_fun, sT_fun, prodT] ---> natT) - end + val T1_fun = T1 --> natT + val T2_fun = T2 --> natT + val prodT = HOLogic.mk_prodT (T1, T2) + in + Const (@{const_name prod_size}, [T1_fun, T2_fun, prodT] ---> natT) + end + +fun snd_const T1 T2 = + Const ("Product_Type.snd", HOLogic.mk_prodT (T1, T2) --> T2) + +fun mk_measure_trm f ctxt T = + HOLogic.dest_setT T + |> fst o HOLogic.dest_prodT + |> f + |> curry (op $) (Const (@{const_name "measure"}, dummyT)) + |> Syntax.check_term ctxt + +(* wf-goal arising in induction_schema *) +fun prove_termination_ind ctxt = + let fun mk_size_measure T = case T of - (Type (@{type_name Sum_Type.sum}, [fT, sT])) => - SumTree.mk_sumcase fT sT natT (mk_size_measure fT) (mk_size_measure sT) - | (Type (@{type_name Product_Type.prod}, [fT, sT])) => - prod_size_const fT sT $ (mk_size_measure fT) $ (mk_size_measure sT) + (Type (@{type_name Sum_Type.sum}, [T1, T2])) => + SumTree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2) + | (Type (@{type_name Product_Type.prod}, [T1, T2])) => + HOLogic.mk_comp (mk_size_measure T2, snd_const T1 T2) | _ => HOLogic.size_const T - fun mk_measure_trm T = - HOLogic.dest_setT T - |> fst o HOLogic.dest_prodT - |> mk_size_measure - |> curry (op $) (Const (@{const_name "measure"}, dummyT)) - |> Syntax.check_term ctxt - - val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral - zero_less_Suc prod.size(1) mult_Suc_right} @ size_simps - val ss' = ss addsimprocs Nat_Numeral_Simprocs.cancel_numerals - in - Function_Relation.relation_tac ctxt mk_measure_trm - THEN_ALL_NEW simp_tac ss' + val measure_trm = mk_measure_trm (mk_size_measure) ctxt + in + Function_Relation.relation_tac ctxt measure_trm end -fun prove_termination size_simps ctxt = - Function.prove_termination NONE - (HEADGOAL (prove_termination_tac size_simps ctxt)) ctxt +(* wf-goal arising in function definitions *) +fun prove_termination_fun size_simps ctxt = +let + fun mk_size_measure T = + case T of + (Type (@{type_name Sum_Type.sum}, [T1, T2])) => + SumTree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2) + | (Type (@{type_name Product_Type.prod}, [T1, T2])) => + prod_size_const T1 T2 $ (mk_size_measure T1) $ (mk_size_measure T2) + | _ => HOLogic.size_const T + + val measure_trm = mk_measure_trm (mk_size_measure) ctxt + + val tac = + Function_Relation.relation_tac ctxt measure_trm + THEN_ALL_NEW simp_tac (size_simpset addsimps size_simps) + in + Function.prove_termination NONE (HEADGOAL tac) ctxt + end (** transformations of premises (in inductive proofs) **)