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