# HG changeset patch # User Andreas Lochbihler # Date 1363695561 -3600 # Node ID bc3651180a09eef8a6ea9cc92307f01faaac1de4 # Parent 67542078fa2159f2e0b5d076d9eb1313142616f0 add induction rule for partial_function (tailrec) diff -r 67542078fa21 -r bc3651180a09 src/HOL/Partial_Function.thy --- a/src/HOL/Partial_Function.thy Mon Mar 18 20:02:37 2013 +0100 +++ b/src/HOL/Partial_Function.thy Tue Mar 19 13:19:21 2013 +0100 @@ -244,6 +244,47 @@ by (rule flat_interpretation) +abbreviation "tailrec_ord \ flat_ord undefined" +abbreviation "mono_tailrec \ monotone (fun_ord tailrec_ord) tailrec_ord" + +lemma tailrec_admissible: + "ccpo.admissible (fun_lub (flat_lub undefined)) (fun_ord tailrec_ord) + (\a. \x. a x \ undefined \ P x (a x))" +proof(intro ccpo.admissibleI[OF tailrec.ccpo] strip) + fix A x + assume chain: "Complete_Partial_Order.chain (fun_ord tailrec_ord) A" + and P [rule_format]: "\f\A. \x. f x \ undefined \ P x (f x)" + and defined: "fun_lub (flat_lub undefined) A x \ undefined" + from defined obtain f where f: "f \ A" "f x \ undefined" + by(auto simp add: fun_lub_def flat_lub_def split: split_if_asm) + hence "P x (f x)" by(rule P) + moreover from chain f have "\f' \ A. f' x = undefined \ f' x = f x" + by(auto 4 4 simp add: Complete_Partial_Order.chain_def flat_ord_def fun_ord_def) + hence "fun_lub (flat_lub undefined) A x = f x" + using f by(auto simp add: fun_lub_def flat_lub_def) + ultimately show "P x (fun_lub (flat_lub undefined) A x)" by simp +qed + +lemma fixp_induct_tailrec: + fixes F :: "'c \ 'c" and + U :: "'c \ 'b \ 'a" and + C :: "('b \ 'a) \ 'c" and + P :: "'b \ 'a \ bool" and + x :: "'b" + assumes mono: "\x. mono_tailrec (\f. U (F (C f)) x)" + assumes eq: "f \ C (ccpo.fixp (fun_lub (flat_lub undefined)) (fun_ord tailrec_ord) (\f. U (F (C f))))" + assumes inverse2: "\f. U (C f) = f" + assumes step: "\f x y. (\x y. U f x = y \ y \ undefined \ P x y) \ U (F f) x = y \ y \ undefined \ P x y" + assumes result: "U f x = y" + assumes defined: "y \ undefined" + shows "P x y" +proof - + have "\x y. U f x = y \ y \ undefined \ P x y" + by(rule tailrec.fixp_induct_uc[of U F C, OF mono eq inverse2])(auto intro: step tailrec_admissible) + thus ?thesis using result defined by blast +qed + + abbreviation "option_ord \ flat_ord None" abbreviation "mono_option \ monotone (fun_ord option_ord) option_ord" @@ -316,13 +357,13 @@ by blast declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun} - @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} NONE *} + @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} + (SOME @{thm fixp_induct_tailrec}) *} declaration {* Partial_Function.init "option" @{term option.fixp_fun} @{term option.mono_body} @{thm option.fixp_rule_uc} (SOME @{thm fixp_induct_option}) *} - hide_const (open) chain end